aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-15put empty_env in hint clause (vo were becoming huge!)barras
2004-09-14majfilliatr
2004-09-14majfilliatr
2004-09-14evar tactic bugfixcorbinea
2004-09-13majfilliatr
2004-09-13* The ML tactic is now also aware of rewriting directions.sacerdot
2004-09-13The ML part of the tactic now knows about covariant and contravariant morphismsacerdot
2004-09-12majfilliatr
2004-09-12majfilliatr
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-10majfilliatr
2004-09-10majfilliatr
2004-09-10simplification de clenvbarras
2004-09-10Dead code removed.sacerdot
2004-09-101. add_new_morphism now has a new optional argument that is the signaturesacerdot
2004-09-10add_new_morphism has now a new argument that is the signaturesacerdot
2004-09-10Add_new_morphism has now a new optional argument that is the signature ofsacerdot
2004-09-10When refining a given term, the primitive refiner used to accepts some casts,sacerdot
2004-09-09majfilliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 03:49:45 +0000