aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...coqbot-app[bot]
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-05Add a redirection from previous location of the proof handling chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-11-05Merge content from two origins into the same file.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
2020-11-05Remove parts of Tactics that were moved elsewhere.Théo Zimmermann
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
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]
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-10-06Documenting option Set Printing Goal Name.Hugo Herbelin
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
2020-09-18Improve `simple apply` exampleMaxime Dénès
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[refman] Replace num by intPierre Roux
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM environm...coqbot
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:34:03 +0000