aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-10-15Wish of Maggesi implemented: the type of the morphism compatibility lemmasacerdot
2004-10-14majfilliatr
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-13majfilliatr
2004-10-13Compatibilité de Hint Rewrite avec Write Stateherbelin
2004-10-12majfilliatr
2004-10-12Desactivation de la construction 'lazy match' en attendant une autre solutionherbelin
2004-10-12Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...herbelin
2004-10-12Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...herbelin
2004-10-12Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...herbelin
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
2004-10-11majfilliatr
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...herbelin
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
2004-10-10majfilliatr
2004-10-08majfilliatr
2004-10-07majfilliatr
2004-10-07setoid_symmetry in ... implemented.sacerdot
2004-10-07New commandssacerdot
2004-10-07iff and impl are now declared as transitive relations.sacerdot
2004-10-07Now Print Setoids prints also the transitivity justification of transitivesacerdot
2004-10-06majfilliatr
2004-10-06* New syntactic sugar: Add Relation ... transitivity proved by ...sacerdot
2004-10-06added transitivitybarras
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-05majfilliatr
2004-10-05majfilliatr
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-04majfilliatr
2004-10-04Added "as ..." parameter to Add Morphism.sacerdot
2004-10-04un paquet de corrections de bugsletouzey
2004-10-03majfilliatr
2004-10-01majfilliatr
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-10-01add_setoid has a new parameter used to synthesize the morphism name.sacerdot
2004-10-01Added "as ..." parameters to "Add Setoid"sacerdot
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
2004-09-30majfilliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 22:28:38 +0000