aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-11-29Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...herbelin
2004-11-29Commit précédent erroné; retour version précédenteherbelin
2004-11-28Suppression bruit perlherbelin
2004-11-28Re-commit version nouvelle syntaxeherbelin
2004-11-28MAJ vis à vis de extratacticsherbelin
2004-11-28Passage à la v8 pour test parserherbelin
2004-11-28Pour ceux qui appelent Makefile avec des fichiers dans des sous-répertoiresherbelin
2004-11-27Complétion déclarations coqideherbelin
2004-11-27Indépendance vis à vis de Symbols (suite)herbelin
2004-11-26Correction bug #879herbelin
2004-11-26Réduire pour trouver l'arité d'une classeherbelin
2004-11-26MAJ PCoFixherbelin
2004-11-26backtrack of the last commit (it was my fault: the code is used bysacerdot
2004-11-26unused function in the interfacesacerdot
2004-11-22Bug commit 1.71herbelin
2004-11-22Code mortherbelin
2004-11-22Correction bug Notation: il faut re-déclarer les règles de parsing des nota...herbelin
2004-11-22Réparation incompatibilité de comportement introduite lors de mise en compa...herbelin
2004-11-22compatibility with POWERPCgregoire
2004-11-21Expansion Case dans injection et discriminate (cf bug #829)herbelin
2004-11-20'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marcheherbelin
2004-11-19Généralisation à Type de certaines propriétés des relationsherbelin
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
2004-11-18Code mortherbelin
2004-11-17Locate Moduleherbelin
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
2004-11-17bug module with ... + vmbarras
2004-11-17Mise en pageherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 14:25:24 +0000