coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-10-28	Remove old compatibility stuff (Tacred.nf)	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-02	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
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