coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest	2006-12-22
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
*	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin	2006-10-03
*	Retour sur la suppression du pf_nf (trop d'exemples utilisent avec	herbelin	2006-10-03
*	Une passe sur l'injection et la discrimination...	herbelin	2006-10-01
*	Suppression de la comparaison (inutile) des paramètres globaux des	herbelin	2006-09-30
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	Correcting for bug #1167	jforest	2006-07-05
*	Updating documentation of replace and correcting a typo in error message of r...	jforest	2006-06-12
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	"subst." works now even when it exists an hypothesis have the form "x=x" in t...	jforest	2006-05-20
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
*	Changement de comportement de rewrite: face a une egalité setoid, on	letouzey	2006-05-02
*	Correction bug 1119 (inversion marche a moitie dans Type)	herbelin	2006-04-02
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Nettoyage coqlib	herbelin	2005-12-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Réparation bug #1004; nettoyage	herbelin	2005-09-08
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	Expansion Case dans injection et discriminate (cf bug #829)	herbelin	2004-11-21
*	Ajout 'dependent rewrite in'	herbelin	2004-10-28
*	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin	2004-10-27
*	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	sacerdot	2004-09-30
*	Proof term size optimization: setoid_rewrite H where H is an application of	sacerdot	2004-09-30
*	New syntax	sacerdot	2004-09-29
*	Correction bug report #855	herbelin	2004-09-24
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...	herbelin	2004-07-30
*	Since setoid_{replace,rewrite} now uses replace there is a circularity	sacerdot	2004-07-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Message d'erreur	herbelin	2004-03-17
*	bug d'Inversion #529 (pb avec ordre d'evaluation)	barras	2004-03-15
*	Retablissement de la correction bug d'inversion faite dans la version 1.116 e...	herbelin	2004-03-12
*	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin	2004-03-11
*	bug de l'inversion (coq-bugs #529)	barras	2004-03-09
*	ne pas échouer si but inchangé pour préserver la compatibilité de 'replace'	herbelin	2004-03-01
*	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin	2004-03-01
*	Ajout 'replace in'	herbelin	2004-03-01
*	Blindage vis a vis des constructeurs partiellement appliques	herbelin	2003-11-18
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Traduction semantique des InHyp de clause en InHypValue si local def; simplif...	herbelin	2003-11-09
*	subst marche dans les deux sens	filliatr	2003-10-17