aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/proof-handling.rst
AgeCommit message (Collapse)Author
2020-11-05Add a redirection from previous location of the proof handling chapter.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-15Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fixcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
Add menu item that uses this
2020-10-06Documenting option Set Printing Goal Name.Hugo Herbelin
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
Fix #12930
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-04Tweak wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-06-04Document known issue of Proof <term> with PG.Théo Zimmermann
See #12444.
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-01-14Document the Set Default Proof Mode command.Pierre-Marie Pédrot
Fixes #10909: Set Default Proof Mode is not documented.
2020-01-08Add note about default goal selector next to bullet docsGaëtan Gilbert
Close #11036
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-10-29Show diffs in "Show Proof."Jim Fehrle
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
It prints a goal given its internal goal id and the Stm state id.
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
Closes GH-8482.
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
Fixes #8320
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: jfehrle
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-28Move content of README-V1-V5 to Credits chapter.Théo Zimmermann
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-10-23Fix formatting. Use standard if..then grammar.Sam Pablo Kuper
2018-10-10Fix names for 2 entries in Flags, Options, Tables index.Jim Fehrle
2018-09-23Documentation for proof diffsJim Fehrle
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-20[doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979Clément Pit-Claudel
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:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-28Add index for focusing braces.Théo Zimmermann
And fix wrong indentation.
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-17Define bullet production token.Théo Zimmermann
2018-08-17Minor Sphinx improvements in the bullet documentation.Théo Zimmermann
And fixing a problem with nested proofs.
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:48:43 +0000