aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
* Affichage numéro de l'état de la commande courante pour mode emacsGravatar herbelin2005-01-14
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ...Gravatar herbelin2004-12-30
* Amélioration message localisation constructions et modulesGravatar herbelin2004-12-09
* Bug (cf #892)Gravatar herbelin2004-12-06
* Amélioration message d'erreur v8Gravatar herbelin2004-12-03
* Complétion commit précédentGravatar herbelin2004-11-29
* Réduire pour trouver l'arité d'une classeGravatar herbelin2004-11-26
* Correction bug Notation: il faut re-déclarer les règles de parsing des nota...Gravatar herbelin2004-11-22
* compatibility with POWERPCGravatar gregoire2004-11-22
* Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREGravatar herbelin2004-11-19
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* *** empty log message ***Gravatar gregoire2004-11-12
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
* Non affichage des notations réduites à une variableGravatar herbelin2004-10-27
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Semble raisonnable de distinguer les noms aussi dans cant_applyGravatar herbelin2004-10-17
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Bug List.hd vs list_lastGravatar herbelin2004-09-03
* MAJ options coqtop et coqcGravatar herbelin2004-09-03
* Pas de notation v7 si purement en v8Gravatar herbelin2004-08-23
* Correction bug #830 : les noms des implicites temporaires étaient inconnus a...Gravatar herbelin2004-08-23
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* "Print Setoids" command added.Gravatar sacerdot2004-07-23
* Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06Gravatar herbelin2004-07-17
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
* Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08Gravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* bug #780: compilation of several units in the same coqtop processGravatar barras2004-07-13
* bug #790: better error_not_cleanGravatar barras2004-07-13
* updated printing of evar context (may loop ?)Gravatar corbinea2004-06-30
* Correction bug #776Gravatar herbelin2004-06-28
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Recherche de la source à partir de la gauche pour gérer des cas comme 'Coer...Gravatar herbelin2004-06-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 04:23:19 +0000