The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

All,

I am fixing an old Coq development, and I'm hitting a snag: one file compiles fine in coqtop but fails with coqc, and I don't understand why, nor do I know how to debug.

coqc --version and coqtop --version return the same thing.

The Coq Proof Assistant, version 8.5pl3 (November 2016)

compiled on Nov 19 2016 16:24:18 with OCaml 4.03.0

cat MyFile.v | coqtop

works like a charm (so does running it in proof general)

but then coqc MyFile.v fails with

File "./MyFile.v", line 161, characters 2-5:

In nested Ltac calls to "lia" and "xlia", last call failed.

Error: Tactic failure:  Cannot find witness.

If I replace lia with omega, it still works with coqtop, still fails with coqc, so it's not just a lia issue.

Error: Omega can't solve this system

Is this a common thing (maybe they use different environment variables or something)?

Is there a way to ask coqc to tell me what is the current state of the goal (-verbose does not help)

Thanks in advance!

Alex