coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New command "Add Relation ..." (for the new implementation of setoid_*).	sacerdot	2004-09-03
*	The old implementation of (setoid_replace c1 with c2) used to replace	sacerdot	2004-09-03
*	V7 .v files for Setoid_* and Ring over setoids commented out.	sacerdot	2004-09-03
*	maj	filliatr	2004-09-02
*	maj	filliatr	2004-09-01
*	maj	filliatr	2004-08-31
*	maj	filliatr	2004-08-30
*	maj	filliatr	2004-08-29
*	maj	filliatr	2004-08-27
*	maj	filliatr	2004-08-26
*	maj	filliatr	2004-08-26
*	Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...	herbelin	2004-08-26
*	maj	filliatr	2004-08-25
*	maj	filliatr	2004-08-24
*	Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1	herbelin	2004-08-24
*	Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...	herbelin	2004-08-24
*	Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...	herbelin	2004-08-24
*	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin	2004-08-24
*	Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...	herbelin	2004-08-24
*	Calling setoid_rewrite on a term H whose type (eq x y) was not an application	sacerdot	2004-08-24
*	maj	filliatr	2004-08-23
*	Précisions message d'erreur	herbelin	2004-08-23
*	Interpretation et affichage corrects des notations LetTuple, affichage des no...	herbelin	2004-08-23
*	Pas de notation v7 si purement en v8	herbelin	2004-08-23
*	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin	2004-08-23
*	The previous test file was truncated. New commit to fix the previous	sacerdot	2004-08-23
*	Amélioration message d'erreur objet de récursion de type non inductif	herbelin	2004-08-06
*	Apply implicit types to local binders too	herbelin	2004-08-06
*	Header V8	herbelin	2004-08-03
*	Protection contre un indice d'evar égal à 0	herbelin	2004-08-03
*	Zbool déjà dans ZArith_base	herbelin	2004-08-03
*	Minimisation utilisation NNPP	herbelin	2004-08-03
*	Déclaration d'obsolescence	herbelin	2004-08-03
*	Typo	herbelin	2004-08-03
*	Ref	herbelin	2004-08-03
*	Bug indexation des Require Import	herbelin	2004-08-03
*	Commentaires coqdoc	herbelin	2004-08-01
*	Commentaires coqdoc	herbelin	2004-08-01
*	Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...	herbelin	2004-07-30
*	MAJ	herbelin	2004-07-30
*	Unbind the macosx dmg after creation to be able to build it again safely	herbelin	2004-07-30
*	maj	filliatr	2004-07-29
*	maj	filliatr	2004-07-29
*	Distinction location ocaml 3.08 ou pas (suite)	herbelin	2004-07-29
*	MAJ cible patch	herbelin	2004-07-29
*	Protection unloc	herbelin	2004-07-29
*	Distinction location ocaml 3.08 ou pas	herbelin	2004-07-29
*	Bug join_loc	herbelin	2004-07-29
*	maj	filliatr	2004-07-28
*	Bug tactique fix	herbelin	2004-07-28