aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-11-07MAJ commentaire sur incohérence EM dans Setherbelin
2004-11-05autorewrite moved from HIGHTACTICS to TACTICS (to implement Printingsacerdot
2004-11-04Univ.pr_univ ==> Univ.pr_unisacerdot
2004-11-04Affichage des universherbelin
2004-11-02Réponse à la conjecture que PI est indépendant de EM dans CCherbelin
2004-10-28qq bugs du highlight de CoqIDEfilliatr
2004-10-28Added code to get rid of duplicate rewriting rules.sacerdot
2004-10-28Ajout 'dependent rewrite in'herbelin
2004-10-27majfilliatr
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-27Ajout test dependent rewriteherbelin
2004-10-27Bug mauvais nom d'entrée binder_constr quand récursion gaucheherbelin
2004-10-27Non affichage des notations réduites à une variableherbelin
2004-10-26majfilliatr
2004-10-25majfilliatr
2004-10-25Word "setoid" banned from the error messages. "relation" used instead.sacerdot
2004-10-25Added option -no-vm.sacerdot
2004-10-25Missing check implemented (closes a bug from Bas Spitters).sacerdot
2004-10-24majfilliatr
2004-10-22majfilliatr
2004-10-21majfilliatr
2004-10-21The morphism lemma type was simplified only in modules and not in modulesacerdot
2004-10-21Error message improved.sacerdot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 20:38:06 +0000