coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq 8.0 errors

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] coq 8.0 errors
Date: Wed, 27 Oct 2004 22:13:44 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Oct 27, 2004 at 03:42:42PM +0200, Stefan Karrmann wrote:

> Lemma sym_t : sym_law T EqT.
> Proof.
>    unfold sym_law, EqT.
>    intros x1 x2 Hx1x2.
>    intros. (* Nothing introduced! Are the let-in's the reason? *)

I think that "destruct x1; destruct x2." will do something sensible
here.

--
Lionel

[Coq-Club] coq 8.0 errors, Stefan Karrmann
- Re: [Coq-Club] coq 8.0 errors, Lionel Elie Mamane
  - [Coq-Club] Still adding modules..., Claudia Fernanda Oliveira K Tavares
    - Re: [Coq-Club] Still adding modules..., Jean-Christophe Filliatre