diff options
| author | Emilio Jesus Gallego Arias | 2020-04-29 15:41:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-29 15:41:03 +0200 |
| commit | b1615099b3b0afff5fa72b1c6ddd835141105653 (patch) | |
| tree | a22e359b2492eabf341a132509b17e3abd4c761b /test-suite/coqdoc/bug11194.html.out | |
| parent | eb45539eb9e757ea5b520ddc06897bcef8f27af8 (diff) | |
| parent | 73e063f18010b4d0a40999782a02333e0baea142 (diff) | |
Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor in record tuples
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite/coqdoc/bug11194.html.out')
| -rw-r--r-- | test-suite/coqdoc/bug11194.html.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out index 6fc6533e59..56bf6eaaca 100644 --- a/test-suite/coqdoc/bug11194.html.out +++ b/test-suite/coqdoc/bug11194.html.out @@ -20,7 +20,7 @@ <div class="code"> <span class="id" title="keyword">Record</span> <a id="a_struct" class="idref" href="#a_struct"><span class="id" title="record">a_struct</span></a> := { <a id="anum" class="idref" href="#anum"><span class="id" title="projection">anum</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> }.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">anum</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">:=</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">0</span></a>|}.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#anum"><span class="id" title="projection">anum</span></a> := 0|}.<br/> <span class="id" title="keyword">Definition</span> <a id="rename_a_s_0" class="idref" href="#rename_a_s_0"><span class="id" title="definition">rename_a_s_0</span></a> := <a class="idref" href="Coqdoc.bug11194.html#a_struct_0"><span class="id" title="definition">a_struct_0</span></a>.<br/> <span class="id" title="keyword">Coercion</span> <a id="some_nat" class="idref" href="#some_nat"><span class="id" title="definition">some_nat</span></a> := (@<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> <span class="id" title="keyword">Definition</span> <a id="rename_some_nat" class="idref" href="#rename_some_nat"><span class="id" title="definition">rename_some_nat</span></a> := <a class="idref" href="Coqdoc.bug11194.html#some_nat"><span class="id" title="definition">some_nat</span></a>.<br/> |