aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-10-20majfilliatr
2004-10-20majfilliatr
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-20bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)barras
2004-10-20The bug already closed in revision 1.90 was reintroduced again.sacerdot
2004-10-19majfilliatr
2004-10-19Proof term size reduction (again).sacerdot
2004-10-18majfilliatr
2004-10-18majfilliatr
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:26:40 +0000