coq/doc/tools, branch master The formal proof system Merge PR #13965: [abbreviation] user syntax to set interp scope of argument 2021-04-23T14:33:27+00:00 Pierre-Marie Pédrot 2021-04-23T14:33:27+00:00 a0c3ebf4a6357a5140b98b4b40c71133c53d802e Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot 
Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphinx output 2021-04-19T09:17:08+00:00 coqbot-app[bot] 2021-04-19T09:17:08+00:00 f82dd4e968d1b948f4288687cb9458ec90b66270 Reviewed-by: Zimmi48 Ack-by: cpitclaudel 
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Merge PR #13815: Improve description of conversions 2021-04-19T09:14:24+00:00 coqbot-app[bot] 2021-04-19T09:14:24+00:00 8a49832ac5a4a9fab564c49ccef7146310db5bab Reviewed-by: Zimmi48 Ack-by: JasonGross 
Reviewed-by: Zimmi48
Ack-by: JasonGross
Include (* ... *) comments in .. coqtop:: directives in Sphinx output 2021-04-17T16:41:42+00:00 Jim Fehrle 2021-02-11T06:56:31+00:00 e038e130188a0b43f66dfbc084cd8d9ca2cfb550 






Remove superfluous sort.
2021-04-17T11:07:41+00:00

Jim Fehrle

2021-04-17T11:07:41+00:00

c20769ad4851ee7fa99605fed6b89964e147cddc

Removing it makes no difference to the order of glossary entries,
which is determined by the "for ... sorted" statement above.





Removing it makes no difference to the order of glossary entries,
which is determined by the "for ... sorted" statement above.







Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.
2021-04-12T17:50:05+00:00

coqbot-app[bot]

2021-04-12T17:50:05+00:00

b78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac

Reviewed-by: jfehrle





Reviewed-by: jfehrle







Remove omega from doc_grammar files.
2021-04-12T14:38:55+00:00

Théo Zimmermann

2021-04-12T14:38:50+00:00

09fb4762de8b2dc256a43d6a931d5a479b98cd26












Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/orange background)
2021-04-10T17:42:13+00:00

coqbot-app[bot]

2021-04-10T17:42:13+00:00

19e991811dc30bd2392cc969667887a159f355e5

Reviewed-by: Zimmi48
Ack-by: cpitclaudel





Reviewed-by: Zimmi48
Ack-by: cpitclaudel







[abbreviation] allow the user to set arguments scope
2021-04-07T17:59:46+00:00

Enrico Tassi

2021-03-19T13:29:07+00:00

d3963fc6b6dad5a0cf79815f31b2035ca8b3de25