aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernac.ml
AgeCommit message (Expand)Author
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-02coqworkmgrEnrico Tassi
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04STM: use sec vars in aux file if no Proof using when building .viEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-10-29Revert the two last commits. My bad, I messed up git-svn commands...ppedrot
2013-10-29Profile only when CAMLRUNPARAM is set.ppedrot
2013-10-29Printing heap on every processed sentence.ppedrot
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
2013-09-12Remove outdated commentgareuselesinge
2013-09-12VernacList handling was lost in STM mergegareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-06Close the .glob file after having saved .vogareuselesinge
2013-04-25Fix compilation (vernac.ml, missing ;)gareuselesinge
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-04-23coqtop -compile: avoid with_heavy_rollback when non-interactiveletouzey
2013-04-17Coqc: repair localisation of errors in filesletouzey
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-14Use Pp.msg instead of Pp.pp in -beautify (loss of text otherwise)letouzey
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 14)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-08catch failures of pr_vernac to make -time failsafegareuselesinge
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-01-28Actually adding backtrace handling.ppedrot
2012-12-14Modulification of dir_pathppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-05coqtop -time : display per-command timingsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
2012-07-11Set/Unset Atomic Load : a pragmatic solution for part 2 of #2820letouzey
2012-07-11Also allow Reset in Load'ed filesletouzey