aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Expand)Author
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
2006-11-01Quick hack to solve to complexity issue in function mark_occurherbelin
2006-10-31Retour sur la modification apportée en r9289, et nouvelle correction du bug ...notin
2006-10-26Affichage d'un message d'erreur losque qu'une relation n'a pas été déclarÃ...notin
2006-10-20Correction du bug #1255 (réécriture setoid sous un produit)notin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
2006-06-06reparation pour le bug #1072 (soufflee par J. Forest): letouzey
2006-05-05encore un correctif sur le rewrite H in setoid: letouzey
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-05resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses letouzey
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-08-19Sur le conseil de X.Leroy: x=[||] devient Array.length x=0letouzey
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
2005-05-19Setoid_replace: improved error message when trying to replace a term in asacerdot
2005-05-19A wish by Bas Spitters granted: a little more of unification up tosacerdot
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-12Changement dans les boxed values .gregoire
2004-10-27Factorisation cut_replacingherbelin
2004-10-25Word "setoid" banned from the error messages. "relation" used instead.sacerdot
2004-10-25Missing check implemented (closes a bug from Bas Spitters).sacerdot
2004-10-21The morphism lemma type was simplified only in modules and not in modulesacerdot
2004-10-21Error message improved.sacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-20The bug already closed in revision 1.90 was reintroduced again.sacerdot
2004-10-19Proof term size reduction (again).sacerdot
2004-10-18* Code simplification and clean-up. In particular there is no more codesacerdot
2004-10-18Code simplification and clean-up.sacerdot
2004-10-18The lem field was not computed properly for morphisms whose argument wassacerdot
2004-10-18The "lem" field of a morphism used to be the compatibility proof, but itsacerdot
2004-10-18Bug fixed: relations quantified more than once where abstracted in the wrongsacerdot
2004-10-18More informative error message when the tactic tries to generate a newsacerdot
2004-10-18zeta flag added to reduce LetIns in a morphism type. Morphisms with localsacerdot
2004-10-15Wrong comment committed. The tactic behaves correctly only when thesacerdot
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
2004-10-14Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newsacerdot
2004-10-14Code clean-up.sacerdot
2004-10-14reflexivity, symmetry, symmetry ... in e transitivity now fall-backsacerdot
2004-10-07setoid_symmetry in ... implemented.sacerdot
2004-10-07New commandssacerdot
2004-10-07Now Print Setoids prints also the transitivity justification of transitivesacerdot
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
2004-10-06added transitivitybarras
2004-10-06Add Setoid now accepts also quantified setoids.sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 06:53:00 +0000