coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2005-09-08	Réparation bug #1004; nettoyage	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-10-27	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin
2004-09-24	Simplifications concommitantes à la correction du bug #855	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-03-11	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin
2004-03-01	Ajout 'replace in'	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-10-11	Death of 'a somewhat cryptic module'	herbelin
2003-05-19	Restructuration des procédures de filtrage	herbelin
2003-03-28	notations <>, Assumption avec existentiel, replace term	mohring
2002-12-17	nouveau Subst:	barras
2002-09-16	Subst (tout court)	filliatr
2002-09-11	tactique Subst x1 ... xn	filliatr
2002-09-09	Code mort de AutoRewrite	herbelin
2002-08-13	AutoRewrite substitutive...	coq
2002-07-17	tactique Subst	filliatr
2002-06-05	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin
2002-06-05	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-03-15	entetes	filliatr
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-05-18	Nettoyage	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-04-30	Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrage	herbelin
2000-04-28	Déplacement du type reference dans Term	herbelin
2000-03-21	Modification de type_of_case, type_case_branches, etc;nettoyage	herbelin
2000-01-21	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr