aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools/coq-commands.rst
AgeCommit message (Expand)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-29Document the -native-compiler optionPierre Roux
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-12Remove documentation of -compile, which was removed in #8690.Théo Zimmermann
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-02Document -rfrom option in reference manual.Théo Zimmermann
2020-04-02Remove deprecated -require option.Théo Zimmermann
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2019-12-12Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...charguer
2019-11-21Document -vos flag for coqdepGaëtan Gilbert
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-21Trivial Sphinx fix in doc.Théo Zimmermann
2018-08-01Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq comman...Zeimer
2018-05-16Minor 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
2018-03-15[Sphinx] Add chapter 14Maxime Dénès
2018-03-15[Sphinx] Move chapter 14 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:59:15 +0000