aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-11-08Insertion de coercion au milieu des applications partielles et propagation de...herbelin
2000-11-08First version with out_variable used. Exports all the standard librarysacerdot
2000-11-08binaires a ingorer par CVSfilliatr
2000-11-08tous les binaires maintenant dans le repertoire binfilliatr
2000-11-08out_variable (Liboject.obj -> ...) distibgue de get_variablefilliatr
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-07Bug sur précédent commitherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-07MAJherbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-11-07Correction sur commit errone de la version 1.3herbelin
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-11-07Orthographeherbelin
2000-11-07MAJherbelin
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06print_idl inlinéherbelin
2000-11-06MAJherbelin
2000-11-06Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-05MAJherbelin
2000-11-05Nouveau mode de compilation de .ml4herbelin
2000-11-05Plus besoin de débrancher la preuve qui ne passait pasherbelin
2000-11-05Plus besoin de rajouter "Require Plus"herbelin
2000-11-05Pour ne plus éviter temporairement le "Auto with zarith" !herbelin
2000-11-05MAJherbelin
2000-11-05Déplacement d'une partie de g_vernac.ml4 dans g_proofs.ml4 car fichier deven...herbelin
2000-11-03Deplacement d'options avec ou sans argtsmohring
2000-11-03Few OCaml files in contrib/xmlsacerdot
2000-11-03compilation avec make de Solaris; README et INSTALLfilliatr
2000-11-03URI problem addressed, but not resolved yetsacerdot
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
2000-10-31.old virés (CVS est là pour ca)filliatr
2000-10-30Ajout d'un switch pour le debuggerdelahaye
2000-10-30Suppression d'Intuition (trop intelligent?)delahaye
2000-10-30Pour eviter temporairement le "Auto with zarith"delahaye
2000-10-30Remplacement de Tauto et Intuitiondelahaye
2000-10-30Tactiques utilisateur + debuggerdelahaye
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
2000-10-30Pour le Require Export (temporaire)delahaye
2000-10-30Ajouts pour les tactiques utilisateurdelahaye
2000-10-28MAJherbelin
2000-10-28Clarification message d'erreurherbelin
2000-10-27MAJherbelin
2000-10-27Passage command -> constrherbelin
2000-10-27Simpl fait trop maintenant; faut adapterherbelin
2000-10-27erreur dans intro_gen corrigéefilliatr
2000-10-27Chasse au Cast de Castherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 17:15:15 +0000