coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin	2000-05-31
*	suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls	herbelin	2000-05-22
*	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin	2000-05-22
*	Restructuration des outils pour les inductifs.	herbelin	2000-05-18
*	Ajout mis_typepath	herbelin	2000-05-16
*	Retrait fullmind de inductive_summary pour simplicité	herbelin	2000-04-27
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
*	Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et...	herbelin	2000-03-21
*	Peaufinement nouveaux types inductive_summary et constructor_summary en vue	herbelin	2000-03-08
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	debug discharge et inductifs	filliatr	1999-12-10
*	Ajout des messages d'erreurs de Cases	herbelin	1999-12-09
*	debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes	filliatr	1999-12-07
*	declarations eliminations / debuggae inductifs (debut)	filliatr	1999-12-06
*	explicitations erreurs inductifs	filliatr	1999-12-05
*	Modification pour faire compiler pretyping.ml qui maintenant compile	herbelin	1999-11-26
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
*	module Wcclausenv	filliatr	1999-11-22
*	module Tactics (debut)	filliatr	1999-11-22
*	module Pattern, Wcclausenv (interface) et Tacticals	filliatr	1999-11-19
*	ensembles de contraintes d'univers	filliatr	1999-09-25
*	suppression champs inutiles dans constantes et inductifs; verification defini...	filliatr	1999-08-27
*	environnement sur	filliatr	1999-08-26
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25