Compilation error with Coq 8.5.2

clarus commented 8 years ago

According to https://coq-bench.github.io/.../8.5.2/mirror-core/1.0.1, the 1.0.1 version of Mirror Core does not compile with Coq 8.5.2 and OCaml 4.03.0:

- "coqc"  -q  -Q "theories" MirrorCore -Q "examples" McExamples -I "src" -I "/home/bench/.opam/system/lib/coq//user-contrib/PluginUtils"   examples/Hoare/ImpSyntax.v
- Makefile.coq:557: recipe for target 'examples/Hoare/ImpSyntax.vo' failed
- make[1]: Leaving directory '/home/bench/.opam/system/build/coq-mirror-core.1.0.1'
- Makefile:2: recipe for target 'coq' failed
- File "./examples/Hoare/ImpSyntax.v", line 392, characters 6-32:
- Error: No such goal.

gmalecha commented 8 years ago

This is fixed by a new release (1.0.2). I have packaged it and submitted a pull request (https://github.com/coq/opam-coq-archive/pull/87)

clarus commented 8 years ago

Thanks!

gmalecha / mirror-core

Compilation error with Coq 8.5.2 #90