coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Nowak <David.Nowak AT irisa.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: 6.2.2 -> 6.2.4 : Implicit Arguments On.
- Date: Thu, 04 Feb 1999 13:42:40 +0100
- Disposition-notification-to: David Nowak <David.Nowak AT irisa.fr>
- Organization: IRISA
Hello,
Usage of «Implicit Arguments» is different from 6.2.2. Does somenone
wrote a script to update from 6.2.2 to 6.2.3/4 (h_convert only deals
with Hint and Auto) ?
Thank you.
------------------------------------------------------------------------
6.2.2 :
Implicit Arguments On.
Inductive P [U:Set] : U->Prop := p: (x:U)(P ? x).
6.2.4 :
Implicit Arguments On.
Inductive P [U:Set] : U->Prop := p: (x:U)(P x).
--
David Nowak
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
David Nowak | phone: +33 2 99 84 25 03
IRISA / INRIA, EP-ATR project | fax: +33 2 99 84 25 28
Campus de Beaulieu | e-mail:
David.Nowak AT irisa.fr
F-35042 RENNES CEDEX - FRANCE | http://www.irisa.fr/prive/nowak/
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- 6.2.2 -> 6.2.4 : Implicit Arguments On., David Nowak
- Re: 6.2.2 -> 6.2.4 : Implicit Arguments On., Patrick Loiseleur
Archive powered by MhonArc 2.6.16.