diff options
| author | Matthew Dempsky | 2020-05-24 19:06:39 -0700 |
|---|---|---|
| committer | Matthew Dempsky | 2020-05-24 19:08:50 -0700 |
| commit | a4f6fdda775c902ecc070038ead3c109f7cd7618 (patch) | |
| tree | 8e4bf36707981c22e26abd5177dcedcf7c8b966a | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Fix hyperlinks in changes.rst
| -rw-r--r-- | doc/sphinx/changes.rst | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5954ded67f..363148e2a0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Changes in 8.11+beta1 dropped when forcing a delayed opaque proof inside a polymorphic section. Also relaxes the nesting criterion for sections, as polymorphic sections can now appear inside a monomorphic one - (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot). + (`#10664 <https://github.com/coq/coq/pull/10664>`_, by Pierre-Marie Pédrot). - **Changed:** Using ``SProp`` is now allowed by default, without needing to pass ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 @@ -476,7 +476,7 @@ Changes in 8.11+beta1 by Vincent Laporte). - **Removed:** Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` - (`#9881 <https://github.com/coq/coq/pull/9811>`_, + (`#9811 <https://github.com/coq/coq/pull/9811>`_, by Vincent Laporte). .. _811Reals: @@ -690,7 +690,7 @@ Changes in 8.11.1 Bump official OCaml support and CI testing to 4.10.0 (`#11131 <https://github.com/coq/coq/pull/11131>`_, `#11123 <https://github.com/coq/coq/pull/11123>`_, - `#11102 <https://github.com/coq/coq/pull/11123>`_, + `#11102 <https://github.com/coq/coq/pull/11102>`_, by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, Guillaume Melquiond, and Guillaume Munch-Maccagnoni). @@ -1091,7 +1091,7 @@ Other changes in 8.10+beta1 e.g., a numeral notation whose parsing function outputs a proof of :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`) - (`#9874 <https://github.com/coq/coq/pull/9840>`_, + (`#9874 <https://github.com/coq/coq/pull/9874>`_, closes `#9840 <https://github.com/coq/coq/issues/9840>`_ and `#9844 <https://github.com/coq/coq/issues/9844>`_, by Jason Gross). @@ -1107,7 +1107,7 @@ Other changes in 8.10+beta1 - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + fixes `#9681 <https://github.com/coq/coq/pull/9681>`_, by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). - The `quote plugin |