index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
usage.ml
Commit message (
Expand
)
Author
Age
*
The -require option now accepts a logical path instead of a physical one.
Pierre-Marie Pédrot
2015-09-25
*
Updating the documentation and the toolchain w.r.t. the change in -compile.
Pierre-Marie Pédrot
2015-09-25
*
For convenience, making yes and on, and no and off synonymous in
Hugo Herbelin
2015-08-02
*
improve --help documentation: the -m|--memory option was missing
Gabriel Scherer
2015-06-24
*
Fix usage about -color.
Pierre Courtieu
2015-05-18
*
Adding an option -w to control Coq warning output.
Pierre-Marie Pédrot
2015-05-14
*
Disable precompilation for native_compute by default.
Guillaume Melquiond
2015-05-14
*
Removing references to deprecated syntax -I/-R -as.
Pierre-Marie Pédrot
2015-03-31
*
coqc: fix --help
Enrico Tassi
2015-03-25
*
add -type-in-type to the usage message
Daniel R. Grayson
2015-03-18
*
Fix typos about .vio files (thanks Arthur for spotting them)
Enrico Tassi
2015-02-12
*
Add -no-native-compiler flag to list dumped by --help.
Maxime Dénès
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
For consistency with other coqtop flags, use -help rather than --help in usage.
Hugo Herbelin
2014-11-16
*
Adding a command line option to print out accepted color tags.
Pierre-Marie Pédrot
2014-11-15
*
Reworking the -color flag of coqtop.
Pierre-Marie Pédrot
2014-11-15
*
toploop plugins taken into account when printing --help (close: 3535)
Enrico Tassi
2014-09-09
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Removing documentation related to the deprecated State machinery.
Pierre-Marie Pédrot
2014-08-16
*
Deprecate useless option -quality.
Guillaume Melquiond
2014-06-13
*
Remove documentation for the unsupported options -byte and -opt.
Guillaume Melquiond
2014-06-13
*
Deprecate options -dont, -lazy, -force-load-proofs.
Guillaume Melquiond
2014-06-13
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Add an option -Q (tentative name).
Guillaume Melquiond
2014-04-08
*
Change handling of loadpath and mlpath.
Guillaume Melquiond
2014-04-06
*
Adding a finer-grained -bt flag to coqtop only triggering backtraces.
Pierre-Marie Pédrot
2013-12-22
*
New option --help-XML-protocol to document the XML procol used by -ideslave
Enrico Tassi
2013-11-27
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Ensure that a function declared with a label is used with it
letouzey
2012-12-08
*
coqtop -time : display per-command timings
letouzey
2012-10-05
*
No more states/initial.coq, instead coqtop now requires Prelude.vo
letouzey
2012-08-23
*
Updating headers.
herbelin
2012-08-08
*
verbose compat notations : nicer option name
letouzey
2012-07-08
*
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2012-07-05
*
Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN
pboutill
2012-06-15
*
coq_makefile fixup
pboutill
2012-06-14
*
New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles
pboutill
2012-06-12
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
-user option removal
pboutill
2011-11-21
*
In Coq_config: get rid of coqsrc and make coqlib optional
glondu
2011-09-27
*
coqtop -config returns coq returns coq environments at exection time
pboutill
2011-04-28
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Ide_slave: a more robust current_status () function
letouzey
2011-03-28
*
CoqIDE argv parsing delegated to coqtop
vgross
2010-09-14
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
* By default, load proof terms.
regisgia
2010-08-31
*
* scripts/Coqc toplevel/Usage:
regisgia
2010-08-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
[next]