coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Changement de subst_meta	mohring	2001-02-28
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Généralisation de constant_opt_value en reference_opt_value	herbelin	2000-11-27
*	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
*	Suppression de Abst	herbelin	2000-09-10
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	Bug existential_value au lieu de existential_type + divers sur existential	herbelin	2000-05-25
*	MAJ modifs Inductive	herbelin	2000-05-18
*	Restructuration des outils pour les inductifs.	herbelin	2000-05-18
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
*	Export mis_typed_arity	herbelin	2000-03-07
*	- environment -> safe_environment	filliatr	1999-12-01
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
*	modules Indrec, Tacentries, Hiddentac	filliatr	1999-11-23
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	module Logic	filliatr	1999-10-14
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	ajout des inductifs (sans types singletons pour l'instant)	filliatr	1999-08-30
*	un petit effort de presentation dans les interfaces	filliatr	1999-08-30
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25