coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange bihaviour with existential variables

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strange bihaviour with existential variables
Date: Tue, 06 Nov 2012 07:03:52 -0500

On 11/06/2012 05:41 AM, Jacques-Henri Jourdan wrote:

Lemma l1 : exists x, pred1 x.
Proof.
eexists.
apply l0.

When trying to execute the last tactic, Coq complains with:

Toplevel input, characters 6-8:
Error: Impossible to unify "(?245 * ?246)%type" with
"tuple (typlst A_constr1)".

Strange indeed: I don't get any error message in Coq 8.4.

[Coq-Club] Strange bihaviour with existential variables, Jacques-Henri Jourdan, 11/06/2012
- Re: [Coq-Club] Strange bihaviour with existential variables, Adam Chlipala, 11/06/2012
- Re: [Coq-Club] Strange bihaviour with existential variables, Thomas Braibant, 11/06/2012
- Re: [Coq-Club] Strange bihaviour with existential variables, Chung-Kil Hur, 11/06/2012
- Re: [Coq-Club] Strange bihaviour with existential variables, Jacques-Henri Jourdan, 11/07/2012
  - Re: [Coq-Club] Strange bihaviour with existential variables, Arnaud Spiwack, 11/07/2012
  - Re: [Coq-Club] Strange bihaviour with existential variables, Chung-Kil Hur, 11/07/2012