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
*
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
*
raise UnsafeSuccess -> feedback AddedAxiom
gareuselesinge
2013-04-25
*
coqtop -compile: avoid with_heavy_rollback when non-interactive
letouzey
2013-04-23
*
Coqc: repair localisation of errors in files
letouzey
2013-04-17
*
Moved the Loadpath part of Library to its own file, and documented
ppedrot
2013-03-26
*
Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)
letouzey
2013-03-14
*
Vernac+Toplevel: get rid of Error_in_file
letouzey
2013-03-13
*
Vernac+Toplevel: get rid of DuringVernacInterp
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 14)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
catch failures of pr_vernac to make -time failsafe
gareuselesinge
2013-03-08
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Modulification of dir_path
ppedrot
2012-12-14
*
Monomorphization (toplevel)
ppedrot
2012-11-26
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
[next]