aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-09-07majfilliatr
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-07* The Coq part of the reflexive tactic setoid_rewrite is generalized tosacerdot
2004-09-06majfilliatr
2004-09-06majfilliatr
2004-09-06mimick: unify types before making assignationbarras
2004-09-06optimized the non-backtracking casebarras
2004-09-06bad env in mimick codebarras
2004-09-06reparation des Extract Constant avec Haskellletouzey
2004-09-05majfilliatr
2004-09-04Correction commit precedentherbelin
2004-09-03majfilliatr
2004-09-03majfilliatr
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-09-03Bug List.hd vs list_lastherbelin
2004-09-03MAJ options coqtop et coqcherbelin
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 syntaxsacerdot
2004-09-03Ported to the new implementation of setoid_*.sacerdot
2004-09-03New reflexive implementation of setoid_rewrite. The new implementationsacerdot
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
2004-09-03The old implementation of (setoid_replace c1 with c2) used to replacesacerdot
2004-09-03V7 .v files for Setoid_* and Ring over setoids commented out.sacerdot
2004-09-02majfilliatr
2004-09-01majfilliatr
2004-08-31majfilliatr
2004-08-30majfilliatr
2004-08-29majfilliatr
2004-08-27majfilliatr
2004-08-26majfilliatr
2004-08-26majfilliatr
2004-08-26Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make depe...herbelin
2004-08-25majfilliatr
2004-08-24majfilliatr
2004-08-24Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1herbelin
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...herbelin
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...herbelin
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...herbelin
2004-08-24Calling setoid_rewrite on a term H whose type (eq x y) was not an applicationsacerdot
2004-08-23majfilliatr
2004-08-23Précisions message d'erreurherbelin
2004-08-23Interpretation et affichage corrects des notations LetTuple, affichage des no...herbelin
2004-08-23Pas de notation v7 si purement en v8herbelin
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus a...herbelin
2004-08-23The previous test file was truncated. New commit to fix the previoussacerdot
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
2004-08-06Apply implicit types to local binders tooherbelin
2004-08-03Header V8herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:37:25 +0000