aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
AgeCommit message (Expand)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphi...coqbot-app[bot]
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Remove superfluous sort.Jim Fehrle
2021-04-12Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.coqbot-app[bot]
2021-04-12Remove omega from doc_grammar files.Théo Zimmermann
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/or...coqbot-app[bot]
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-30Remove the :> type castJim Fehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-12Fixed grammar productions for PDF documentationsIsaac Oscar Gariano
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-04Correctly sort the glossaryJim Fehrle
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
2020-12-09Allow any character in a tacn, cmd, ... nameJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
2020-11-16Update grammar in docJim Fehrle
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
2020-11-15Merge PR #13368: Fix dune rules for @check-gram following recent changes.coqbot-app[bot]
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve d...coqbot-app[bot]
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:16 +0000