aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
AgeCommit message (Expand)Author
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-04Timeout message was not always displayedbarras
2009-03-04commande Timeout + compaction des traces de debug_tacticbarras
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-14Fixing/improving management of uniform prefix Local and Globalherbelin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-04-23Added frozen state after each command.courtieu
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2006-12-28Cleaning backtracking code, optimized "Backtrack n x y" when n iscourtieu
2006-11-21Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deherbelin
2006-09-12Indentation + svnpropnotin
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...notin
2005-12-27Autres suppressions de composantes du traducteurherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-05-15Globalisation des Tactic Notationherbelin
2005-02-06Nettoyage et documentation de Libraryherbelin
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
2004-07-16Nouvelle en-têteherbelin
2004-05-25Correction bug 'Time Load foo'herbelin
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2004-01-22Protection table des locations lors de Load (pour coqdoc)herbelin
2003-12-24*** empty log message ***barras
2003-11-18Bug: faut brancher la sortie des tactiques sur stdout pendant traductionherbelin
2003-11-09Mise en place traduction des tactiques apres evaluation pour permettre des ch...herbelin
2003-10-20bug traduction de auto.(simpl). en auto.simpl.barras
2003-10-16oups! ca compile maintenantbarras
2003-10-16translator avoids printing a . followed by a ( by inserting a spacebarras
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-03pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitherbelin
2003-09-24Traduction aussi si -translate et -load-vernac-sourceherbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-18Plutôt que de faire "Load" silencieusement, en profiter pour traduireherbelin
2003-09-16Pour cacher le contenu de Load au traducteurherbelin
2003-09-10Debranchement du traducteur pour Load !herbelin
2003-09-02Freeze mal placeherbelin
2003-08-12Bug et amliorations diversesherbelin
2003-06-23Ajout systématique de Proof dans la traductionherbelin
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ...herbelin
2003-05-13Affichage commentairesherbelin