coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin	2009-08-06
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau	2009-06-30
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau	2008-11-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Even better test for choosing rewrite or setoid_rewrite.	msozeau	2008-07-26
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau	2008-04-12
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Rework on rich forms of rewrite	letouzey	2008-03-01
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest	2007-05-17
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Une passe sur l'injection et la discrimination...	herbelin	2006-10-01
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	Réparation bug #1004; nettoyage	herbelin	2005-09-08
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin	2004-10-27
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin	2004-03-11
*	Ajout 'replace in'	herbelin	2004-03-01
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	nouveau Subst:	barras	2002-12-17
*	Subst (tout court)	filliatr	2002-09-16
*	tactique Subst x1 ... xn	filliatr	2002-09-11
*	Code mort de AutoRewrite	herbelin	2002-09-09
*	AutoRewrite substitutive...	coq	2002-08-13
*	tactique Subst	filliatr	2002-07-17
*	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-06-05
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	entetes	filliatr	2001-03-15
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12