aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.ml
AgeCommit message (Expand)Author
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
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-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
2010-08-31* By default, load proof terms.regisgia
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
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:44:08 +0000