aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)Gravatar barras2004-10-20
* The bug already closed in revision 1.90 was reintroduced again.Gravatar sacerdot2004-10-20
* majGravatar filliatr2004-10-19
* Proof term size reduction (again).Gravatar sacerdot2004-10-19
* majGravatar filliatr2004-10-18
* majGravatar filliatr2004-10-18
* * Code simplification and clean-up. In particular there is no more codeGravatar sacerdot2004-10-18
* Code simplification and clean-up.Gravatar sacerdot2004-10-18
* The lem field was not computed properly for morphisms whose argument wasGravatar sacerdot2004-10-18
* The "lem" field of a morphism used to be the compatibility proof, but itGravatar sacerdot2004-10-18
* Bug fixed: relations quantified more than once where abstracted in the wrongGravatar sacerdot2004-10-18
* More informative error message when the tactic tries to generate a newGravatar sacerdot2004-10-18
* zeta flag added to reduce LetIns in a morphism type. Morphisms with localGravatar sacerdot2004-10-18
* Tacred après TypingGravatar herbelin2004-10-18
* majGravatar filliatr2004-10-17
* Semble raisonnable de distinguer les noms aussi dans cant_applyGravatar herbelin2004-10-17
* Vérification de la typability de 'pattern'Gravatar herbelin2004-10-17
* *** empty log message ***Gravatar herbelin2004-10-17
* majGravatar filliatr2004-10-15
* majGravatar filliatr2004-10-15
* Wrong comment committed. The tactic behaves correctly only when theGravatar sacerdot2004-10-15
* 2 bugs de reconnaissanceGravatar coq2004-10-15
* Wish of Maggesi implemented: the type of the morphism compatibility lemmaGravatar sacerdot2004-10-15
* majGravatar filliatr2004-10-14
* Bug fixed (reported by Maggesi): sometimes when the tactic had to generate newGravatar sacerdot2004-10-14
* Code clean-up.Gravatar sacerdot2004-10-14
* reflexivity, symmetry, symmetry ... in e transitivity now fall-backGravatar sacerdot2004-10-14
* majGravatar filliatr2004-10-13
* Compatibilité de Hint Rewrite avec Write StateGravatar herbelin2004-10-13
* majGravatar filliatr2004-10-12
* Desactivation de la construction 'lazy match' en attendant une autre solutionGravatar herbelin2004-10-12
* Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...Gravatar herbelin2004-10-12
* Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...Gravatar herbelin2004-10-12
* Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...Gravatar herbelin2004-10-12
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* majGravatar filliatr2004-10-11
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...Gravatar herbelin2004-10-11
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* majGravatar filliatr2004-10-10
* majGravatar filliatr2004-10-08
* majGravatar filliatr2004-10-07
* setoid_symmetry in ... implemented.Gravatar sacerdot2004-10-07
* New commandsGravatar sacerdot2004-10-07
* iff and impl are now declared as transitive relations.Gravatar sacerdot2004-10-07
* Now Print Setoids prints also the transitivity justification of transitiveGravatar sacerdot2004-10-07
* majGravatar filliatr2004-10-06
* * New syntactic sugar: Add Relation ... transitivity proved by ...Gravatar sacerdot2004-10-06
* added transitivityGravatar barras2004-10-06
* added transitivityGravatar barras2004-10-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:31:24 +0000