aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.mli
AgeCommit message (Expand)Author
2014-09-18Fix debug printing with primitive projections.Matthieu Sozeau
2014-09-16Undo prints only if coqtop || emacsEnrico Tassi
2014-09-09Undo: if the ui is coqtop (command line) then Undo is not part of the doc.Enrico Tassi
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-02coqworkmgrEnrico Tassi
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-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-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-01-26CoqIDE: command line for extra coqtop "flags"Enrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
2013-10-03STM: number of slaves passed by the command linegareuselesinge
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
2013-08-08Coqide ported to STMgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
2013-06-02Flags V8_4 for compatibility infrastructure.herbelin
2013-05-28Setting "appcontext" as the default behaviour in Ltac matching.ppedrot
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
2013-04-25Flag ide_slave moved into Flags modulegareuselesinge
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-08-08Updating headers.herbelin
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-04Added a color output to Coqtop.ppedrot
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
2012-04-26Program: avoid staying in program mode after a failed Program commandletouzey
2012-03-14Second step of integration of Program:msozeau
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-07-29Rather quick hack to make basic unicode notations available byherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:34:53 +0000