coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Stefan Monnier" <monnier+lists.coq/news/ AT rum.cs.yale.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Instantiating "existential" ?2730 meta-variable
Date: 10 Dec 2002 12:02:52 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Newsgroups: lists.coq

It seems silly, but I can't seem to figure out how to prove

  (iptr r n)=(iptr ?2570 ?2571)

I though that the Reflexivity tactic would of course do the job
but it says:

  Error: w_Unify

Any idea what's going on ?

        Stefan

[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