aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.ml
Commit message (Expand)AuthorAge
* More work on error handlingGravatar letouzey2011-05-17
* Repair the "Fail" command after recent changes in exception handlingGravatar letouzey2011-05-16
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
* Fail, when successful, prints something only in verbose modeGravatar glondu2010-10-26
* Avoid raising an anomaly when an error encapsulated with a dummyGravatar herbelin2010-10-03
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Timeout message was not always displayedGravatar barras2009-03-04
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
* Added frozen state after each command.Gravatar courtieu2008-04-23
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
* Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms deGravatar herbelin2006-11-21
* Indentation + svnpropGravatar notin2006-09-12
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Abstraction vis à vis du type loc pour compatibilité ocaml 3.08Gravatar herbelin2004-07-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Correction bug 'Time Load foo'Gravatar herbelin2004-05-25
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
* modif des fixpoints pour que si on donne une notation au produit, les pts fix...Gravatar barras2004-03-05
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* Protection table des locations lors de Load (pour coqdoc)Gravatar herbelin2004-01-22
* *** empty log message ***Gravatar barras2003-12-24
* Bug: faut brancher la sortie des tactiques sur stdout pendant traductionGravatar herbelin2003-11-18
* Mise en place traduction des tactiques apres evaluation pour permettre des ch...Gravatar herbelin2003-11-09
* bug traduction de auto.(simpl). en auto.simpl.Gravatar barras2003-10-20
* oups! ca compile maintenantGravatar barras2003-10-16
* translator avoids printing a . followed by a ( by inserting a spaceGravatar barras2003-10-16
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10