aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-11-17bug module M:=N avec vmbarras
2004-11-17Ajout 'Locate Module'herbelin
2004-11-17Bug 'Locate Library lib' quand 'lib' est aussi un moduleherbelin
2004-11-17Déclaration de '..' comme mot-clé (résoud bug #856)herbelin
2004-11-17Message d'erreurherbelin
2004-11-17Suppression capture des variables par lieurs non liés dans Notation; simplif...herbelin
2004-11-17Suppression capture des variables par lieurs non liés dans Notationherbelin
2004-11-17Test lieurs dans Notationherbelin
2004-11-17test-suite/output/Notations.outherbelin
2004-11-16Copy of the definition of prodT (already in the standard library) removed.sacerdot
2004-11-16dead (and obsolete) code (in comments) removedsacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-11-15bug coqmktop avec libcoqrun.a en bytecodebarras
2004-11-15Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...herbelin
2004-11-12*** empty log message ***gregoire
2004-11-12Changement dans les boxed values .gregoire
2004-11-10Correction bug #868herbelin
2004-11-09MAJherbelin
2004-11-09code mortherbelin
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 13:24:01 +0000