aboutsummaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
AgeCommit message (Expand)Author
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
2016-05-19fix blanks in usage messageEnrico Tassi
2016-05-19coqc: support -o option to specify output file nameEnrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-02For convenience, making yes and on, and no and off synonymous inHugo Herbelin
2015-06-24Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-24improve --help documentation: the -m|--memory option was missingGabriel Scherer
2015-06-22All invocations to ocaml compilers go through ocamlfindPierre Boutillier
2015-05-18Fix usage about -color.Pierre Courtieu
2015-05-14Adding an option -w to control Coq warning output.Pierre-Marie Pédrot
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-03-25coqc: fix --helpEnrico Tassi
2015-03-18add -type-in-type to the usage messageDaniel R. Grayson
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-01-12Add -no-native-compiler flag to list dumped by --help.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-11-16For consistency with other coqtop flags, use -help rather than --help in usage.Hugo Herbelin
2014-11-15Adding a command line option to print out accepted color tags.Pierre-Marie Pédrot
2014-11-15Reworking the -color flag of coqtop.Pierre-Marie Pédrot
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-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.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-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-11-27New option --help-XML-protocol to document the XML procol used by -ideslaveEnrico Tassi
2013-08-22Misc changes around coqtop.ml :letouzey
2012-12-08Ensure that a function declared with a label is used with itletouzey
2012-10-05coqtop -time : display per-command timingsletouzey
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-08Updating headers.herbelin
2012-07-08verbose compat notations : nicer option nameletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-15Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BINpboutill
2012-06-14coq_makefile fixuppboutill
2012-06-12New step in purpose to get both camlp4 and camlp5 compatible coq_makefilespboutill
2012-04-12lib directory is cut in 2 cma.pboutill
2011-11-21-user option removalpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:25:36 +0000