aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
AgeCommit message (Expand)Author
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-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
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-22Removing some generic equalities.ppedrot
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-22Misc changes around coqtop.ml :letouzey
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-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-02-24New -no-native-compiler flag for configure, globally disabling the nativemdenes
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-11-13Small uniformization in Stringppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-08-08Updating headers.herbelin
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-07Colorization of coqtop messages is turned *off* by defaultletouzey
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-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:05:10 +0000