The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I think you should definitely report this to https://coq.inria.fr/bugs/

If you can, make a small example that reproduces the bug, and attach it 
to the bug report.

-- Jonathan


On 11/20/2016 02:36 PM, Alexandre Pilkiewicz wrote:
> After figuring it out that I can print goals with Print. and fail right
> after, I found out the difference.
> The tactic
> autounfold with autounfold in *.
> does less unfolding in coqc. In particular, it does not unfold in coqc (but
> does in coqtop) a function defined like this:
>
> Definition Pol_In v (pol: Polyhedron) :=
>    list_forall (satisfy_constraint v) pol.
>
> I manually unfold it and the proof now passes in both, but it still is
> quite weird.
>
> Alex
>
> On Sun, Nov 20, 2016 at 8:09 PM, Alexandre Pilkiewicz <
> alexandre.pilkiewicz AT polytechnique.org>
>  wrote:
>
> > 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