index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.mli
Commit message (
Expand
)
Author
Age
*
[vernac] Move `Quit` and `Drop` to the toplevel layer.
Emilio Jesus Gallego Arias
2018-03-11
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
|
[toplevel] Move beautify to its own pass.
Emilio Jesus Gallego Arias
2018-02-28
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
[toplevel] Make toplevel state into a record.
Emilio Jesus Gallego Arias
2018-02-15
*
[flags] Move global time flag into an attribute.
Emilio Jesus Gallego Arias
2017-12-23
*
Separate vernac controls and regular commands.
Maxime Dénès
2017-12-20
*
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
Emilio Jesus Gallego Arias
2017-10-11
*
[stm] Switch to a functional API
Emilio Jesus Gallego Arias
2017-10-06
*
[stm] [flags] Move document mode flags to the STM.
Emilio Jesus Gallego Arias
2017-10-06
*
[flags] Remove XML output flag.
Emilio Jesus Gallego Arias
2017-08-01
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[toplevel] Remove unused parameter from `Vernac.process_expr`.
Emilio Jesus Gallego Arias
2017-04-25
*
[stm] Port the toplevel to the STM.
Emilio Jesus Gallego Arias
2017-04-12
*
[toplevel] Remove undocumented "just_parsing" flag.
Emilio Jesus Gallego Arias
2016-10-17
*
Vernac.ml: inlining read_vernac_file within load_vernac.
Hugo Herbelin
2016-10-17
*
Applying Emilio's suggestion to simplify type of eval_expr.
Hugo Herbelin
2016-10-17
*
Attaching all extra imperative components of the lexer/parser state to
Hugo Herbelin
2016-10-09
*
Add file name, line number and beginning of line position to locations.
Maxime Dénès
2016-06-20
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Fix coqc -time (Closes: 3201)
Enrico Tassi
2014-01-05
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
raise UnsafeSuccess -> feedback AddedAxiom
gareuselesinge
2013-04-25
*
Vernac+Toplevel: get rid of Error_in_file
letouzey
2013-03-13
*
Vernac+Toplevel: get rid of DuringVernacInterp
letouzey
2013-03-13
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
Updating headers.
herbelin
2012-08-08
*
A new status Unsafe in Interface. Meant for commands such as Admitted.
aspiwack
2012-07-12
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
A unified backtrack mechanism, with a basic "Show Script" as side-effect
letouzey
2012-03-23
*
Noise for nothing
pboutill
2012-03-02
*
Fixing bugs #2347 (part 2) and #2388: error message printing was done
herbelin
2010-09-18
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Delineating a API for Coq inside toplevel/vernac.ml
vgross
2010-02-12
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout entree pour exporter les debuts et fins de compilation en mode -xml
herbelin
2004-03-26
*
Localisation des erreurs d'internalisation des notations de tactiques
herbelin
2004-02-12
*
Undo dans Coq IDE
filliatr
2003-02-11
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
[next]