coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	conflit useInversionLemma	mohring	2000-12-13
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	caractere opaque des constantes repris en compte	filliatr	2000-12-04
*	nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...	filliatr	2000-11-06
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	suppression des (* open Generic *)	filliatr	2000-11-02
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	Renommage canonique :	herbelin	2000-10-18
*	Abstraction de constr	herbelin	2000-09-14
*	Correction pour make doc	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Plus de env et sigma dans get_arity, plus de sigma dans make_arity	herbelin	2000-07-01
*	Extension de find_inductive aux co-inductifs et renommage en find_rectype	herbelin	2000-07-01
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	Nettoyage	herbelin	2000-05-18
*	Rien	herbelin	2000-05-16
*	Intégration de leminv	herbelin	2000-05-05
*	Intégration progressive	herbelin	2000-04-30
*	Inversion (pas termine)	filliatr	2000-03-27