coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Intros and delta reduction

From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
To: casteran AT labri.u-bordeaux.fr (Pierre Casteran)
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Intros and delta reduction
Date: Wed, 16 Jan 2002 00:47:53 +0100 (MET)

  Hi Pierre,

> Then Intros id1 ... idN can no more described as equivalent to Intro i1;
> Intro i2; ... ; Intro iN.

  You're right. There is an inconsistency wrt documentation that we will fix.

  Hugo

PS: please use http://coq.inria.fr/bin/coq-bugs or ;
coq-bugs AT pauillac.inria.fr

for bug reports.

[Coq-Club] Intros and delta reduction, Pierre Casteran
- Re: [Coq-Club] Intros and delta reduction, Hugo Herbelin