coq - The formal proof system

Age	Commit message (Expand)	Author
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-26	Even better test for choosing rewrite or setoid_rewrite.	msozeau
2008-06-21	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2008-03-01	Rework on rich forms of rewrite	letouzey
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
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