coq - The formal proof system

Age	Commit message (Expand)	Author
2004-01-27	Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...	herbelin
2003-11-22	Bug introduit avec le 'Simpl f'	herbelin
2003-11-09	Ajout reduce_to_quantified_ref	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-30	Mise au point de declare_red_expr	herbelin
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modÃ¨le d'analyse syntaxique et d'interprÃ©tation des tactiques et co...	herbelin
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-09-09	Nettoyage reduce_to_ind et one_step_reduce	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-03-15	entetes	filliatr
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-09-14	Minor correction for Ocamlweb + doc update	coq
2000-09-14	DÃ©placement de fonctions de Reduction vers Tacred	herbelin
1999-12-15	Nouveaux types 'constructor' et 'inductive' dans Term;	herbelin
1999-12-13	- Ã©tats fabriquÃ©s avec -silent	filliatr
1999-12-02	modifs pour premiere edition de liens	filliatr