| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle | |
| 2021-01-01 | Merge PR #13470: Convert rewriting and proof-mode chapters to prodn | coqbot-app[bot] | |
| Reviewed-by: Zimmi48 Ack-by: JasonGross | |||
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle | |
| 2020-12-29 | Document the -native-compiler option | Pierre Roux | |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann | |
| The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version. | |||
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann | |
| 2020-08-04 | Document "Print Debug GC" command and OCAMLRUNPARAM env variable | Jim Fehrle | |
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle | |
| 2020-05-14 | Merge PR #12097: Interleave commandline require/set/unset commands | Emilio Jesus Gallego Arias | |
| Ack-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2020-05-13 | Document the changes regarding the order of command-line options. | Théo Zimmermann | |
| 2020-05-12 | Remove documentation of -compile, which was removed in #8690. | Théo Zimmermann | |
| 2020-04-11 | Merge PR #11961: Convert vernac commands chapter to prodn, update syntax | Théo Zimmermann | |
| Ack-by: Zimmi48 Ack-by: cpitclaudel | |||
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle | |
| 2020-04-02 | Document -rfrom option in reference manual. | Théo Zimmermann | |
| So far it was only documented in coqtop --help. | |||
| 2020-04-02 | Remove deprecated -require option. | Théo Zimmermann | |
| This option is confusing because it does Require Import, not Require. It was deprecated in 8.11. We remove it in 8.12 in order to reintroduce it in 8.13 as a replacement for -load-vernac-object, which is the option that does Require without Import as of today. | |||
| 2020-03-21 | Reorder the load/require cmd-options and set/unset cmd-options | Lasse Blaauwbroek | |
| Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line. The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed, then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag. | |||
| 2020-01-29 | [rfc] [mltop] Removal of dynamic loading of object and `.ml` files | Emilio Jesus Gallego Arias | |
| This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome. | |||
| 2019-12-12 | Fix #11195 and add other improvements: try loading .vio (and not just .vo) ↵ | charguer | |
| if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio. | |||
| 2019-11-21 | Document -vos flag for coqdep | Gaëtan Gilbert | |
| 2019-11-21 | Merge PR #11075: load .vo when .vos is missing + misc vos changes | Emilio Jesus Gallego Arias | |
| Reviewed-by: gares Reviewed-by: silene | |||
| 2019-11-20 | From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing ↵ | charguer | |
| (fixing bug #11057). With this new behavior, it is not needed to .vos files in user contribs. Also, this commit adds a feature: upon creation of a .vo file, an empty .vok file is touched. | |||
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle | |
| 2019-11-01 | Add warnings regarding the experimental nature of the vos feature in the doc. | Pierre-Marie Pédrot | |
| 2019-11-01 | fix coq_makefile and doc for vos support. | charguer | |
| 2019-11-01 | additional details in the doc for -vos | charguer | |
| 2019-11-01 | Implementing support for vos/vok files. | charguer | |
| A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file. | |||
| 2019-06-08 | Mini fix documentation coqtop in passing. | Hugo Herbelin | |
| 2019-06-08 | Documenting new options -require-import, -require-export, etc. | Hugo Herbelin | |
| Slight improving of style in passing. | |||
| 2019-04-16 | Command-line setters for options | Gaëtan Gilbert | |
| TODO coqproject handling (for now it can be done through -arg I guess) | |||
| 2019-02-18 | Sphinx: fail when a command fails | Gaëtan Gilbert | |
| This uses a new coqtop-only option "Coqtop Exit On Error", not sure where to put the doc for it. It being an option means we can locally turn it off (.. coqtop:: fail). | |||
| 2019-01-30 | [toplevel] Deprecate the `-compile` flag in favor of `coqc`. | Emilio Jesus Gallego Arias | |
| This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments. | |||
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-09-23 | Documentation for proof diffs | Jim Fehrle | |
| 2018-09-20 | [doc] Include the rst and LaTeX preambles automatically in all files | Clément Pit-Claudel | |
| 2018-08-31 | Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵ | Zeimer | |
| directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues. | |||
| 2018-08-28 | Merge PR #8281: Trivial Sphinx fix in doc. | Clément Pit-Claudel | |
| 2018-08-22 | Fix #8251: remove "the the" occurrences | Gaëtan Gilbert | |
| 2018-08-21 | Trivial Sphinx fix in doc. | Théo Zimmermann | |
| 2018-08-01 | Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq ↵ | Zeimer | |
| commands' of the Reference Manual. | |||
| 2018-05-16 | Minor update of the documentation/man about the resource file. | Hugo Herbelin | |
| 2018-05-05 | [sphinx] Fix a typo that appeared during the migration. | Théo Zimmermann | |
| 2018-04-14 | [Sphinx] Fix all remaining warnings. | Maxime Dénès | |
| 2018-04-14 | [sphinx] Fix many warnings. | Théo Zimmermann | |
| Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | |||
| 2018-03-15 | [Sphinx] Add chapter 14 | Maxime Dénès | |
| Thanks to Paul Steckler for porting this chapter. | |||
| 2018-03-15 | [Sphinx] Move chapter 14 to new infrastructure | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |