aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernac.mli
Commit message (Expand)AuthorAge
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [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