aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
* vi2vo: new flag -schedule-vi2voGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* -schedule-vi-checking ported to spawnGravatar Enrico Tassi2014-01-26
* break > 80 cols lineGravatar Enrico Tassi2014-01-26
* CoqIDE: ported to spawnGravatar Enrico Tassi2014-01-26
* -schedule-vi-checking generates better scriptGravatar Enrico Tassi2014-01-14
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* .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