coq/test-suite/coqdoc, branch master The formal proof system Fix broken HTML rendering of inference rules (fix #12783). 2020-12-28T10:26:54+00:00 Guillaume Melquiond 2020-12-28T09:29:34+00:00 aed648afd2cf8b09d67fb39c9672b71166089395 






Coqdoc: we move a newline at a better place.
2020-11-14T21:55:47+00:00

Hugo Herbelin

2020-11-05T15:17:37+00:00

696df507b58800a7a6b52741fd4ed859aff7b1c3

This does not affect the rendering but gives better structured
html/tex files.





This does not affect the rendering but gives better structured
html/tex files.







Addressing #13304: how to verbatim an expression mentioning >>.
2020-11-14T21:55:47+00:00

Hugo Herbelin

2020-11-05T12:08:14+00:00

7923bb570cd493aff31ac1c94f9e03ff4efd465f

We clarify that there are two kinds of verbatim: inline and block.

We add a test testing verbatim and others.

Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>





We clarify that there are two kinds of verbatim: inline and block.

We add a test testing verbatim and others.

Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>







coqdoc: Fix the “details” environment
2020-07-29T15:48:22+00:00

Thomas Letan

2020-07-29T12:53:19+00:00

ce233d5b4a6f8d506c37a2a492679a66f9618a94

The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.





The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.







Fix coqdoc bad bulleting from incorrect space count
2020-07-24T10:02:14+00:00

Gaëtan Gilbert

2020-07-24T09:29:36+00:00

e140848fd50a49aab7810eb369c9e14efe20f2d6

Fix #12742





Fix #12742







Fixing #3451: coqdoc links for projections of tuples rather than for constructor.
2020-04-21T17:29:57+00:00

Hugo Herbelin

2020-04-05T16:20:36+00:00

ab14dab1f8a612e3d854df89ae6d21c26ebb2945

Moreover, the link to the constructor was hiding other contents of the
tuple.





Moreover, the link to the constructor was hiding other contents of the
tuple.







Granting coqdoc wish #7093 (definitions link to themselves).
2020-04-20T16:58:15+00:00

Hugo Herbelin

2020-04-05T14:47:01+00:00

e41be40fb1675311801f8c7f7039a44575a45fff

Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>





Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>







Coqdoc: Exporting location and unique id for binding variables.
2020-04-15T17:45:39+00:00

Hugo Herbelin

2020-04-06T08:04:42+00:00

3f2742b2c3fd48706d4bfd8bffdd4ae07a338bbd

This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.

In particular, this fixes #7697.





This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.

In particular, this fixes #7697.







Fixes #11194 (Canonical/Coercion not located for coqdoc).
2020-04-05T13:43:04+00:00

Hugo Herbelin

2020-04-05T13:22:18+00:00

825f001fc03f94ee8076a33e34312f5d4a76eafb

The location was missing in the parser.





The location was missing in the parser.







[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorations
2020-01-14T13:20:18+00:00

Karl Palmskog

2020-01-13T20:59:22+00:00

6b05ae1c447680cd4ed1332c0c8b4f0e24b33f03