Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problem with translation of Hurkens.v file #4

Open
ejgallego opened this issue Jan 21, 2019 · 0 comments
Open

Problem with translation of Hurkens.v file #4

ejgallego opened this issue Jan 21, 2019 · 0 comments

Comments

@ejgallego
Copy link

When trying to export Hurkens.v, I get:

Exporting Coq.Logic.Hurkens
Debug: Vernac Interpreter Executing command
File "/home/egallego/external/CoqInE/test/Test.v", line 57, characters 0-19:
Error: Anomaly "in Univ.repr: Universe Var(1) undefined."
Please report at http://coq.inria.fr/bugs/.
frame @ file "toplevel/coqtop.ml", line 489, characters 15-50
frame @ file "list.ml", line 117, characters 24-34
frame @ file "toplevel/vernac.ml", line 224, characters 30-94
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 99, characters 19-40
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "toplevel/vernac.ml", line 103, characters 31-46
frame @ file "stm/stm.ml", line 2646, characters 11-49
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 2635, characters 4-55
frame @ file "stm/stm.ml", line 2525, characters 4-100
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 934, characters 6-10
frame @ file "stm/stm.ml", line 2398, characters 16-43
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "stm/stm.ml", line 1087, characters 12-91
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacentries.ml", line 2344, characters 4-36
raise @ unknown
frame @ file "vernac/vernacentries.ml", line 2311, characters 8-666
frame @ file "lib/flags.ml", line 99, characters 19-40
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "lib/flags.ml", line 17, characters 14-17
frame @ file "vernac/vernacentries.ml", line 2158, characters 30-66
raise @ file "clib/exninfo.ml", line 65, characters 2-15
frame @ file "vernac/vernacinterp.ml", line 80, characters 4-18
frame @ file "src/commands.ml4", line 24, characters 4-20
frame @ file "list.ml", line 106, characters 12-15
frame @ file "src/libraries.ml", line 23, characters 6-68
frame @ file "list.ml", line 106, characters 12-15
frame @ file "list.ml", line 106, characters 12-15
frame @ file "src/modules.ml", line 43, characters 20-89
frame @ file "kernel/typeops.ml", line 442, characters 19-28
frame @ file "kernel/typeops.ml", line 435, characters 10-28
frame @ file "kernel/typeops.ml", line 366, characters 16-31
frame @ file "kernel/typeops.ml", line 366, characters 16-31
frame @ file "kernel/typeops.ml", line 366, characters 16-31
frame @ file "kernel/typeops.ml", line 366, characters 16-31
frame @ file "kernel/typeops.ml", line 366, characters 16-31
frame @ file "kernel/typeops.ml", line 350, characters 20-42
frame @ file "array.ml", line 101, characters 21-40
frame @ file "kernel/typeops.ml", line 358, characters 12-25
frame @ file "kernel/typeops.ml", line 125, characters 11-35
frame @ file "kernel/environ.ml", line 190, characters 2-65
frame @ file "set.ml", line 352, characters 25-28
frame @ file "kernel/uGraph.ml", line 633, characters 13-21
frame @ file "kernel/uGraph.ml", line 136, characters 22-115
raise @ file "lib/loc.ml", line 89, characters 16-23

Makefile:33: recipe for target 'generate' failed
make: *** [generate] Error 129
make: se sale del directorio '/home/egallego/external/CoqInE/test'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant