aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
AgeCommit message (Expand)Author
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-09Load Prelude.vi if not Prelude.vo is found (Close: 3595)Enrico Tassi
2014-09-09toploop plugins taken into account when printing --help (close: 3535)Enrico Tassi
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-02coqworkmgrEnrico Tassi
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-07-10option to always delegate futures to workersEnrico Tassi
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico Tassi
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Deprecate useless option -unsafe.Guillaume Melquiond
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-02-26vi2vo: new flag -schedule-vi2voEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-26break > 80 cols lineEnrico Tassi
2014-01-26CoqIDE: ported to spawnEnrico Tassi
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-11-27New option --help-XML-protocol to document the XML procol used by -ideslaveEnrico Tassi
2013-10-07coqtop: init STM before loading rcfilegareuselesinge
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
2013-10-03STM: number of slaves passed by the command linegareuselesinge
2013-09-19Made the filename of compiled files explicit, i.e. add a ./ prefixppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
2013-04-23minor cleanup in coqtop.mlletouzey
2013-04-23Coqtop -compile : avoid saving init state when compiling just one fileletouzey
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 17:02:15 +0000