diff options
Diffstat (limited to 'html-test/ref/mini_Test.html')
| -rw-r--r-- | html-test/ref/mini_Test.html | 36 |
1 files changed, 12 insertions, 24 deletions
diff --git a/html-test/ref/mini_Test.html b/html-test/ref/mini_Test.html index 26db2c0f..8cd3321a 100644 --- a/html-test/ref/mini_Test.html +++ b/html-test/ref/mini_Test.html @@ -20,11 +20,9 @@ window.onload = function () {pageLoad();}; ></div ><div id="interface" ><h1 - >Type declarations -</h1 + >Type declarations</h1 ><h2 - >Data types -</h2 + >Data types</h2 ><div class="top" ><p class="src" ><span class="keyword" @@ -130,8 +128,7 @@ window.onload = function () {pageLoad();}; > a b</p ></div ><h2 - >Records -</h2 + >Records</h2 ><div class="top" ><p class="src" ><span class="keyword" @@ -149,8 +146,7 @@ window.onload = function () {pageLoad();}; > </p ></div ><h1 - >Class declarations -</h1 + >Class declarations</h1 ><div class="top" ><p class="src" ><span class="keyword" @@ -184,8 +180,7 @@ window.onload = function () {pageLoad();}; > a</p ></div ><h1 - >Function types -</h1 + >Function types</h1 ><div class="top" ><p class="src" ><a href="" target="main" @@ -193,11 +188,9 @@ window.onload = function () {pageLoad();}; ></p ></div ><h1 - >Auxiliary stuff -</h1 + >Auxiliary stuff</h1 ><h1 - >A hidden module -</h1 + >A hidden module</h1 ><div class="top" ><p class="src" ><a href="" target="main" @@ -205,11 +198,9 @@ window.onload = function () {pageLoad();}; ></p ></div ><h1 - >A visible module -</h1 + >A visible module</h1 ><h1 - >Existential / Universal types -</h1 + >Existential / Universal types</h1 ><div class="top" ><p class="src" ><span class="keyword" @@ -219,8 +210,7 @@ window.onload = function () {pageLoad();}; > a</p ></div ><h1 - >Type signatures with argument docs -</h1 + >Type signatures with argument docs</h1 ><div class="top" ><p class="src" ><a href="" target="main" @@ -240,11 +230,9 @@ window.onload = function () {pageLoad();}; ></p ></div ><h1 - >A section -</h1 + >A section</h1 ><h2 - >A subsection -</h2 + >A subsection </h2 ><div class="top" ><p class="src" ><a href="" target="main" |