aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* code mortGravatar herbelin2004-11-09
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
* MAJ commentaire sur incohérence EM dans SetGravatar herbelin2004-11-07
* autorewrite moved from HIGHTACTICS to TACTICS (to implement PrintingGravatar sacerdot2004-11-05
* Univ.pr_univ ==> Univ.pr_uniGravatar sacerdot2004-11-04
* Affichage des universGravatar herbelin2004-11-04
* Réponse à la conjecture que PI est indépendant de EM dans CCGravatar herbelin2004-11-02
* qq bugs du highlight de CoqIDEGravatar filliatr2004-10-28
* Added code to get rid of duplicate rewriting rules.Gravatar sacerdot2004-10-28
* Ajout 'dependent rewrite in'Gravatar herbelin2004-10-28
* majGravatar filliatr2004-10-27
* Factorisation cut_replacingGravatar herbelin2004-10-27
* Restructuration fonctions de réécriture depuis égalité dépendanteGravatar herbelin2004-10-27
* Restructuration fonctions de réécriture depuis égalité dépendante; facto...Gravatar herbelin2004-10-27
* Ajout test dependent rewriteGravatar herbelin2004-10-27
* Bug mauvais nom d'entrée binder_constr quand récursion gaucheGravatar herbelin2004-10-27
* Non affichage des notations réduites à une variableGravatar herbelin2004-10-27
* majGravatar filliatr2004-10-26
* majGravatar filliatr2004-10-25
* Word "setoid" banned from the error messages. "relation" used instead.Gravatar sacerdot2004-10-25
* Added option -no-vm.Gravatar sacerdot2004-10-25
* Missing check implemented (closes a bug from Bas Spitters).Gravatar sacerdot2004-10-25
* majGravatar filliatr2004-10-24
* majGravatar filliatr2004-10-22
* majGravatar filliatr2004-10-21
* The morphism lemma type was simplified only in modules and not in moduleGravatar sacerdot2004-10-21
* Error message improved.Gravatar sacerdot2004-10-21
* majGravatar filliatr2004-10-20
* majGravatar filliatr2004-10-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 01:49:50 +0000