Multiple definition of the extension constructor name Found.

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

http://coq.inria.fr/

GNU Lesser General Public License v2.1

27 stars 5 forks source link

Multiple definition of the extension constructor name Found. #127

Open IFEIFEI opened 3 years ago

IFEIFEI commented 3 years ago

While I was trying to execute make, this happens.

OCAMLOPT  kernel/univ.ml
File "kernel/univ.ml", line 302, characters 16-21:
Error: Multiple definition of the extension constructor name Found.
       Names must be unique in a given structure or signature.
make[1]: *** [kernel/univ.cmx] Error 2
make[1]: Leaving directory `/home/dany/workplace/coq-trunk'
make: *** [world] Error 2

ybertot commented 3 years ago

You have to give information about the compilation setup. What were all the commands you executed to get to this error message?