coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Stefan Monnier <monnier+lists/coq AT rum.cs.yale.edu>
Cc: Stefan Monnier <monnier+lists.coq/news/ AT rum.cs.yale.edu>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable
Date: Tue, 10 Dec 2002 19:46:45 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Dec 10, 2002 at 12:33:04PM -0500, Stefan Monnier wrote:
> > > (iptr r n)=(iptr ?2570 ?2571)

>> Lemma xeqx: (A:Set)(x:A)(x=x).
>> And use "Apply xeqx.".

> It makes no difference: I also get `Error: w_Unify'.

Hmm... Well, I had a case where the lemma (P:Prop)P->P help, so I
thought maybe something like that would here.

There still is the obvious: At the "EApply" that introduced these
metavariables, instantiate them (EApply Baz with foo:=r bar:=n)
instead of letting the metavariable come in the first place.

--
Lionel

[Coq-Club] Instantiating "existential" ?2730 meta-variable, Stefan Monnier
- Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Lionel Elie Mamane
  - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Stefan Monnier
    - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Lionel Elie Mamane
      - Re: [Coq-Club] Instantiating "existential" ?2730 meta-variable, Claudio Sacerdoti Coen