aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...herbelin
2004-12-06MAJ affichage nouvelle syntaxeherbelin
2004-12-06Commentaireherbelin
2004-12-06Bug (cf #892)herbelin
2004-12-05MAJherbelin
2004-12-05MAJ changements ChoiceFactsherbelin
2004-12-05MAJherbelin
2004-12-05Paramétrisation du domaine des axiomes de choix + ajout description = choice...herbelin
2004-12-04Bug 'set n in * |-'herbelin
2004-12-04Failed in 8.0pl1herbelin
2004-12-03Orthographe!herbelin
2004-12-03Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...herbelin
2004-12-03Was failing in 8.0pl1herbelin
2004-12-03Amélioration message d'erreur v8herbelin
2004-12-01pp of nested fixpoints (dangling with/for)barras
2004-11-30Export pr_intro_patternherbelin
2004-11-29UserError in reduce_to_*_refherbelin
2004-11-29Complétion commit précédentherbelin
2004-11-29*** empty log message ***gregoire
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 12:51:01 +0000