aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
AgeCommit message (Expand)Author
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
2004-10-06* code clean upsacerdot
2004-10-06Th unification procedure has been made a bit more complete by recording thesacerdot
2004-10-06Leibniz equality is now a quantified relation.sacerdot
2004-10-05* code simplificationsacerdot
2004-10-05* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whethersacerdot
2004-10-05* Bug fix: in case of non dependent implications the second argument wassacerdot
2004-10-01eq_constr replaced with a conversion test where possible.sacerdot
2004-10-011. added new parameter "as ..." to Add Setoid. Used to synthesize the namesacerdot
2004-09-30New tacticsacerdot
2004-09-30New tactic [setoid_]rewrite ... in ... [generate side conditions ...].sacerdot
2004-09-30Proof term size optimization: setoid_rewrite H where H is an application ofsacerdot
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
2004-09-30setoid_replace E1 with E2sacerdot
2004-09-29* error messages improvedsacerdot
2004-09-29Add Relation is now able to detect non well typed relation registrations.sacerdot
2004-09-29The Add Morphism command is now able to detect in advance:sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:55:49 +0000