aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-18Tacred après Typingherbelin
2004-10-17majfilliatr
2004-10-17Semble raisonnable de distinguer les noms aussi dans cant_applyherbelin
2004-10-17Vérification de la typability de 'pattern'herbelin
2004-10-17*** empty log message ***herbelin
2004-10-15majfilliatr
2004-10-15majfilliatr
2004-10-15Wrong comment committed. The tactic behaves correctly only when thesacerdot
2004-10-152 bugs de reconnaissancecoq
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 09:00:18 +0000