aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-06Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-01-31Bug lié au dischargeherbelin
2001-01-31Ajout option Set/Unset/Test Printing Coercionsherbelin
2001-01-31Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...herbelin
2001-01-30Branchement sur Objdefherbelin
2001-01-30Les Objdef introduisent une convertibilité avec les projections dans le test...herbelin
2001-01-30backtrack sur le lexeur de la V6filliatr
2001-01-29pas de warning avec Opaque quand is_silentfilliatr
2001-01-27make docherbelin
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Réorganisation suite ajout de constantes locales dans les Recordsherbelin
2001-01-24Ajout de constantes locales dans les Recordsherbelin
2001-01-18Bug Identity Coercionherbelin
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-27Bug installation non localeherbelin
2000-12-25Bug discharge process_classherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert afi...herbelin
2000-12-19correction de bugs sur commit précédentherbelin
2000-12-19Découpage des différentes fonctionnalités de build_mutual et definition_st...herbelin
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
2000-12-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
2000-12-15 - suppression mind_extract_paramsfilliatr
2000-12-15Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...herbelin
2000-12-15Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...herbelin
2000-12-15Printermohring
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif d'u...herbelin
2000-12-14Amélioration message d'erreurherbelin
2000-12-14Raffinement erreur Wrong Predicateherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-12petit bug -byte/-opt (execv -> execvp) et message coercion teste is_silentfilliatr
2000-12-06Ajout erreur DoesNotOccurInherbelin
2000-12-06Suppresion de l'option -as, c'est maintenant -R qui devient l'option standard...herbelin
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
2000-12-05Mini-nettoyage noms longsherbelin
2000-12-04caractere opaque des constantes repris en comptefilliatr
2000-11-30Changement de la syntaxe des options -I et -Rherbelin
2000-11-29Bug option -I et -R quand le répertoire est '..'herbelin
2000-11-29Bug option -I et -R quand le répertoire est '.'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-27 04:42:44 +0000