aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Adding a finer-grained -bt flag to coqtop only triggering backtraces.Gravatar Pierre-Marie Pédrot2013-12-22
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
* New option --help-XML-protocol to document the XML procol used by -ideslaveGravatar Enrico Tassi2013-11-27
* coqtop: init STM before loading rcfileGravatar gareuselesinge2013-10-07
* STM: add options to disable fallbacks to ease regression testingGravatar gareuselesinge2013-10-03
* STM: number of slaves passed by the command lineGravatar gareuselesinge2013-10-03
* Made the filename of compiled files explicit, i.e. add a ./ prefixGravatar ppedrot2013-09-19
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Safe_typing code refactoringGravatar letouzey2013-08-20
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Flag ide_slave moved into Flags moduleGravatar gareuselesinge2013-04-25
* minor cleanup in coqtop.mlGravatar letouzey2013-04-23
* Coqtop -compile : avoid saving init state when compiling just one fileGravatar letouzey2013-04-23
* Remove deprecated option -no-hash-consing (currently doing nothing)Gravatar letouzey2013-04-23
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Fixed parsing of -no-native-compiler flag.Gravatar mdenes2013-01-24
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Using library string functions.Gravatar ppedrot2012-12-13
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
* Restoring flush of Welcome message lost in r15148Gravatar herbelin2012-12-06
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Another GC testGravatar ppedrot2012-11-13
* Removed the modification of the GC pressure coefficient, in orderGravatar ppedrot2012-11-12
* Coq is a heavy user of persistent data structures and symbolic ASTs, so theGravatar ppedrot2012-11-06
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
* Avoid [Loading ML file ...] messages when launching coqtopGravatar letouzey2012-09-07
* Use fully-qualified Coq.Init.Prelude when starting coqtopGravatar letouzey2012-08-24
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* Updating headers.Gravatar herbelin2012-08-08
* verbose compat notations : nicer option nameGravatar letouzey2012-07-08
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Colorization of coqtop messages is turned *off* by defaultGravatar letouzey2012-06-07
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* Added a color output to Coqtop.Gravatar ppedrot2012-06-04
* Fixed printing error problem... A line had disappeared in a previous patch.Gravatar ppedrot2012-06-02
* Flushing formatters before program exit.Gravatar ppedrot2012-06-02
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01