aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
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-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-19Add style for 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 #13185: Add missing ";" in Record grammarcoqbot-app[bot]
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]
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-10-06Documenting option Set Printing Goal Name.Hugo Herbelin
2020-10-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
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]
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]
2020-10-02More details in the documentation of native arraysVincent Semeria
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
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
2020-09-18Improve `simple apply` exampleMaxime Dénès
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra s...coqbot-app[bot]
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-11[numeral notation] Improve documentationPierre Roux
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Explicit integer and naturalPierre Roux
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
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
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-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:40:00 +0000