coq - The formal proof system

Age	Commit message (Expand)	Author
2004-09-03	Bug List.hd vs list_last	herbelin
2004-09-03	MAJ options coqtop et coqc	herbelin
2004-09-03	* New test (for setoid_replace in the general case)	sacerdot
2004-09-03	* setoid_test.v removed and added again in new syntax	sacerdot
2004-09-03	Ported to the new implementation of setoid_*.	sacerdot
2004-09-03	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot
2004-09-03	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-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	maj	filliatr
2004-08-26	Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...	herbelin
2004-08-25	maj	filliatr
2004-08-24	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-23	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-06	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-03	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-01	Commentaires coqdoc	herbelin
2004-08-01	Commentaires coqdoc	herbelin
2004-07-30	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-29	maj	filliatr
2004-07-29	maj	filliatr
2004-07-29	Distinction location ocaml 3.08 ou pas (suite)	herbelin