index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernac.ml
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
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
*
|
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
|
/
*
Remove some uses of Loadpath.get_paths.
Guillaume Melquiond
2015-09-29
*
The -compile option now accepts ".v" files and outputs a warning otherwise.
Pierre-Marie Pédrot
2015-09-25
*
Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)
Guillaume Melquiond
2015-07-28
*
Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its
Hugo Herbelin
2015-07-07
*
Splitting the library representation on disk in two.
Pierre-Marie Pédrot
2015-06-24
*
coqtop: reset the current file name after a load-vernac-source
Enrico Tassi
2015-05-29
*
make Unset Silent work in coqc
Enrico Tassi
2015-05-29
*
Adding an option -w to control Coq warning output.
Pierre-Marie Pédrot
2015-05-14
*
STM: process_error_hook set in Vernac where fname is known (fix #4229)
Enrico Tassi
2015-05-12
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Update headers.
Maxime Dénès
2015-01-12
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Removing a pperrnl.
Pierre-Marie Pédrot
2014-11-15
*
Goal printing made uniform: always done in STM (close 3585)
Enrico Tassi
2014-10-22
*
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
coqworkmgr
Enrico Tassi
2014-09-02
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Remove the syntax [Vernac1. Vernac2. … Vernacn. ].
Arnaud Spiwack
2014-06-06
*
STM: make -async-proofs on work from coqc too
Enrico Tassi
2014-03-18
*
Stm: smarter delegation policy
Enrico Tassi
2014-03-12
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
Fix coqc -time (Closes: 3201)
Enrico Tassi
2014-01-05
*
coqtop: -check-vi-tasks and -schedule-vi-checking
Enrico Tassi
2014-01-05
*
STM: use sec vars in aux file if no Proof using when building .vi
Enrico Tassi
2014-01-04
*
.vi files: .vo files without proofs
Enrico Tassi
2014-01-04
*
Revert the two last commits. My bad, I messed up git-svn commands...
ppedrot
2013-10-29
*
Profile only when CAMLRUNPARAM is set.
ppedrot
2013-10-29
*
Printing heap on every processed sentence.
ppedrot
2013-10-29
*
STM: some refactoring, support revised CoqIDE protocol
gareuselesinge
2013-09-30
*
Remove outdated comment
gareuselesinge
2013-09-12
*
VernacList handling was lost in STM merge
gareuselesinge
2013-09-12
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
Simple machinery to detect EXTEND that interpret during parsing
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Close the .glob file after having saved .vo
gareuselesinge
2013-05-06
*
Fix compilation (vernac.ml, missing ;)
gareuselesinge
2013-04-25
[next]