aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/setoid_replace.ml
Commit message (Expand)AuthorAge
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Quick hack to solve to complexity issue in function mark_occurGravatar herbelin2006-11-01
* Retour sur la modification apportée en r9289, et nouvelle correction du bug ...Gravatar notin2006-10-31
* Affichage d'un message d'erreur losque qu'une relation n'a pas été déclarÃ...Gravatar notin2006-10-26
* Correction du bug #1255 (réécriture setoid sous un produit)Gravatar notin2006-10-20
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* reparation pour le bug #1072 (soufflee par J. Forest): Gravatar letouzey2006-06-06
* encore un correctif sur le rewrite H in setoid: Gravatar letouzey2006-05-05
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses Gravatar letouzey2006-04-05
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
* New commit to allow definitions of morphisms on relations whose carrier isGravatar sacerdot2005-05-24
* Setoid_replace: improved error message when trying to replace a term in aGravatar sacerdot2005-05-19
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of theGravatar sacerdot2005-01-18
* Bug fixed (reported by Roland): the setoire_rewrite in tactic did not workGravatar sacerdot2005-01-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Factorisation cut_replacingGravatar herbelin2004-10-27
* Word "setoid" banned from the error messages. "relation" used instead.Gravatar sacerdot2004-10-25
* Missing check implemented (closes a bug from Bas Spitters).Gravatar sacerdot2004-10-25
* The morphism lemma type was simplified only in modules and not in moduleGravatar sacerdot2004-10-21
* Error message improved.Gravatar sacerdot2004-10-21
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* The bug already closed in revision 1.90 was reintroduced again.Gravatar sacerdot2004-10-20
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
* Code simplification and clean-up.Gravatar sacerdot2004-10-18
* The lem field was not computed properly for morphisms whose argument wasGravatar sacerdot2004-10-18
* The "lem" field of a morphism used to be the compatibility proof, but itGravatar sacerdot2004-10-18
* Bug fixed: relations quantified more than once where abstracted in the wrongGravatar sacerdot2004-10-18
* More informative error message when the tactic tries to generate a newGravatar sacerdot2004-10-18
* zeta flag added to reduce LetIns in a morphism type. Morphisms with localGravatar sacerdot2004-10-18
* Wrong comment committed. The tactic behaves correctly only when theGravatar sacerdot2004-10-15
* Wish of Maggesi implemented: the type of the morphism compatibility lemmaGravatar sacerdot2004-10-15
* Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newGravatar sacerdot2004-10-14
* Code clean-up.Gravatar sacerdot2004-10-14
* reflexivity, symmetry, symmetry ... in e transitivity now fall-backGravatar sacerdot2004-10-14
* setoid_symmetry in ... implemented.Gravatar sacerdot2004-10-07
* New commandsGravatar sacerdot2004-10-07
* Now Print Setoids prints also the transitivity justification of transitiveGravatar sacerdot2004-10-07
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* added transitivityGravatar barras2004-10-06
* Add Setoid now accepts also quantified setoids.Gravatar sacerdot2004-10-06