aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernac.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[toplevel] Move beautify to its own pass.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[toplevel] Remove unused parameter from `Vernac.process_expr`.Emilio Jesus Gallego Arias
2017-04-12[stm] Port the toplevel to the STM.Emilio Jesus Gallego Arias
2016-10-17[toplevel] Remove undocumented "just_parsing" flag.Emilio Jesus Gallego Arias
2016-10-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
2016-10-09Attaching all extra imperative components of the lexer/parser state toHugo Herbelin
2016-06-20Add file name, line number and beginning of line position to locations.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
2012-10-05coqtop -time : display per-command timingsletouzey
2012-08-08Updating headers.herbelin
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-02Noise for nothingpboutill
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2004-07-16Nouvelle en-têteherbelin
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:10:48 +0000