coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	nouvelle implantation de la reduction	barras	2001-03-01
*	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin	2001-02-07
*	Bug env vis à vis du let in	herbelin	2000-12-15
*	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
*	Renommage AppL en App	herbelin	2000-10-01
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
*	Correction pour make doc	herbelin	2000-09-10
*	Suppression de Abst	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
*	Modifs d'interpretation de patterns	delahaye	2000-07-21
*	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
*	Achèvement abstraction du mécanisme (optionnel) de cast	herbelin	2000-06-29
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
*	Nettoyage de Generic	herbelin	2000-05-31
*	Effets de bords suite à la restructuration des inductives (cf Inductive)	herbelin	2000-05-18
*	Réorganisation	herbelin	2000-05-05
*	Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)	herbelin	2000-05-04
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...	herbelin	2000-03-21
*	MAJ nouveau try_mutind_of	herbelin	2000-03-08
*	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin	1999-12-15
*	Intégration initiale du Cases	herbelin	1999-12-11
*	Ajout des messages d'erreurs de Cases	herbelin	1999-12-09
*	Retour dans pretyping	herbelin	1999-12-01