aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2020-11-05Remove parts of Tactics that were moved elsewhere.Théo Zimmermann
2020-11-05Keep only the content on solvers for logic and equality.Théo Zimmermann
2020-11-05Move some content to a new page on solvers for logic and equality.Théo Zimmermann
2020-11-05Keep only content about auto.Théo Zimmermann
2020-11-05Move some content to a new page on automation.Théo Zimmermann
2020-11-05Add new page to writing proof index.Théo Zimmermann
2020-11-05Remove everything before term rewriting and simplification.Théo Zimmermann
2020-11-05Remove everything after term rewriting and simplification.Théo Zimmermann
2020-11-05Move some content to a new page on term rewriting and simplification.Théo Zimmermann
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
2020-11-05[refman] Add an example for number notationsPierre Roux
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:27:14 +0000