aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.mli
Commit message (Expand)AuthorAge
* [toplevel] Remove unused parameter from `Vernac.process_expr`.Gravatar Emilio Jesus Gallego Arias2017-04-25
* [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
* Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
* Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
* Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
* Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Fix coqc -time (Closes: 3201)Gravatar Enrico Tassi2014-01-05
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* raise UnsafeSuccess -> feedback AddedAxiomGravatar gareuselesinge2013-04-25
* Vernac+Toplevel: get rid of Error_in_fileGravatar letouzey2013-03-13
* Vernac+Toplevel: get rid of DuringVernacInterpGravatar letouzey2013-03-13
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
* Updating headers.Gravatar herbelin2012-08-08
* A new status Unsafe in Interface. Meant for commands such as Admitted.Gravatar aspiwack2012-07-12
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Noise for nothingGravatar pboutill2012-03-02
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
* Localisation des erreurs d'internalisation des notations de tactiquesGravatar herbelin2004-02-12
* Undo dans Coq IDEGravatar filliatr2003-02-11
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Ajout d'une option et d'une fonction compile pour fabriquer les .voGravatar herbelin2001-09-18
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* corrections pour ocamlwebGravatar filliatr1999-09-28
* retablissement du toplevelGravatar filliatr1999-09-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 11:51:24 +0000