coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	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
*	Proposition de correction pour le bug #1173 (ou du moins pour un	herbelin	2007-04-13
*	Changement mineur du comportement de 'rewrite .. in * \|-': si le	notin	2007-03-30
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
*	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