aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-12-06MAJ affichage nouvelle syntaxeherbelin
2004-12-04Bug 'set n in * |-'herbelin
2004-11-26backtrack of the last commit (it was my fault: the code is used bysacerdot
2004-11-26unused function in the interfacesacerdot
2004-11-22Réparation incompatibilité de comportement introduite lors de mise en compa...herbelin
2004-11-21Expansion Case dans injection et discriminate (cf bug #829)herbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-15Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...herbelin
2004-11-12Changement dans les boxed values .gregoire
2004-10-28Added code to get rid of duplicate rewriting rules.sacerdot
2004-10-28Ajout 'dependent rewrite in'herbelin
2004-10-27Factorisation cut_replacingherbelin
2004-10-27Restructuration fonctions de réécriture depuis égalité dépendanteherbelin
2004-10-27Restructuration fonctions de réécriture depuis égalité dépendante; facto...herbelin
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-13Compatibilité de Hint Rewrite avec Write Stateherbelin
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 11:07:53 +0000