coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with notations

From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
To: "Jevgenijs Sallinens" <jevgenijs AT dva.lv>
Cc: "Jacek Chrzaszcz" <chrzaszc AT mimuw.edu.pl>, "Pierre Casteran" <casteran AT labri.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] problem with notations
Date: Thu, 15 Jan 2004 16:02:48 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, 15 Jan 2004 16:15:06 +0200
"Jevgenijs Sallinens"
<jevgenijs AT dva.lv>
wrote:

> Lemma Nat_1x : (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).

If you put NA2.NA.eq_Nat instead of eq_Nat in the type of the lemme, then
the script works works... Don't understand why this is necessary.

Pierre

[Coq-Club] problem with notations, Houda Anoun
- Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
  - Re: [Coq-Club] problem with notations, Pierre Casteran
    - Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
    - Re: [Coq-Club] problem with notations, Houda Anoun
      - Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
- <Possible follow-ups>
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens
  - Re: [Coq-Club] problem with notations, Pierre Courtieu
  - Re: [Coq-Club] problem with notations, Houda Anoun
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens
  - Re: [Coq-Club] problem with notations, Pierre Casteran
  - Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens