aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-09-09Créditherbelin
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-09-08majfilliatr
2004-09-08majfilliatr
2004-09-08unification encore...barras
2004-09-08* cleaning/renaming in Setoids.vsacerdot
2004-09-08* cleaning/renamingsacerdot
2004-09-08The innersort is now computed as the more precise sort between thesacerdot
2004-09-08The code used to compare the synthesized and the expected type (if available)sacerdot
2004-09-08The Coq part of the reflexive part can now deal with irreflexive relations too.sacerdot
2004-09-08The Coq part of the reflexive tactic is now able to handle alsosacerdot
2004-09-08petit bug avec les effets de bordsbarras
2004-09-08Meilleur anglais (cf #841)herbelin
2004-09-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...herbelin
2004-09-07majfilliatr
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