aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.mli
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-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
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-10-04Changed the way to support compatibility with previous versions.herbelin
2009-09-22Add the option to automatically introduce variables declared before themsozeau
2009-08-14Tried to make F1 documentation tool working in CoqIDE.herbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-08Suite 10904 (fichiers oubliés)herbelin