aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-10-19Add style for smallcaps.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
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 #13185: Add missing ";" in Record grammarcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-10-12Add missing ";" in record grammarJim Fehrle
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-10Documenting the new only-parsing only-printing model.Hugo Herbelin
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-10-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-02Merge PR #13125: More details in the documentation of native arrayscoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: Blaisorblade Ack-by: herbelin
2020-10-02More details in the documentation of native arraysVincent Semeria
Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Add persistent data structure Update doc/sphinx/language/core/primitive.rst Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Update doc/sphinx/language/core/primitive.rst Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
A commit at 2003-03-13 changed the lemma name. https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
Instead, the example was duplicated.
2020-09-18Improve `simple apply` exampleMaxime Dénès
The example showing the difference between `apply` and `simple apply` used to depend on the order and the heuristics used on unification problems. We make it independent for better clarity and stability. Fixes https://github.com/coq/coq/issues/13023
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra ↵coqbot-app[bot]
spaces in notations Reviewed-by: jfehrle
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-11[numeral notation] Improve documentationPierre Roux
Following reviews from Jim Fehrle on #12218 and #12979
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11[refman] Explicit integer and naturalPierre Roux
As respectively bigint and bignat that fit into an OCaml int.
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[refman] Replace num by intPierre Roux
num stands for natural numbers whereas the text deals with negative values.
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-08[Small typo] Update match.rstClément Blaudeau
Some error messages were merged together
2020-09-08Merge PR #12927: Explain that tactics applied to multiple goals don't ↵coqbot-app[bot]
preserve the order Reviewed-by: Zimmi48 Ack-by: chdoc Ack-by: jfehrle
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-09-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: JasonGross
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
Fix #12930
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-26Merge PR #12884: Documentation of coq_makefile: fix name of installation dir ↵coqbot-app[bot]
+ help on using option -f Reviewed-by: jfehrle Ack-by: herbelin
2020-08-25Documentation of coq_makefile: fix name of installation dir + help on option -f.Hugo Herbelin
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 11:49:41 +0000