diff options
author | Ben Gamari <ben@smart-cactus.org> | 2016-05-10 18:09:50 +0200 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2016-05-10 18:13:25 +0200 |
commit | 5731f3b94f560eb2e604871609c7ea139e932ad2 (patch) | |
tree | 17d6430482274a8d46db055dfae48afc1400b50d /html-test/ref/PatternSyns.html | |
parent | 88bacd21107ef9b8d8d83d5d281a06c8ef4f2271 (diff) |
html-test: Update reference output
Diffstat (limited to 'html-test/ref/PatternSyns.html')
-rw-r--r-- | html-test/ref/PatternSyns.html | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/html-test/ref/PatternSyns.html b/html-test/ref/PatternSyns.html index ffebdf27..70e9230b 100644 --- a/html-test/ref/PatternSyns.html +++ b/html-test/ref/PatternSyns.html @@ -91,13 +91,13 @@ window.onload = function () {pageLoad();setSynopsis("mini_PatternSyns.html& >(:<->)</a > :: <span class="keyword" >forall</span - > t t. t -> t -> (<a href="#" + > t t1. t -> t1 -> (<a href="#" >FooType</a > t, <a href="#" >FooType</a > (<a href="#" >FooType</a - > t))</li + > t1))</li ><li class="src short" ><span class="keyword" >data</span @@ -113,9 +113,9 @@ window.onload = function () {pageLoad();setSynopsis("mini_PatternSyns.html& >E</a > :: <span class="keyword" >forall</span - > k t t. <a href="#" + > k t t1. <a href="#" >(><)</a - > k t t</li + > k t t1</li ></ul ></div ><div id="interface" @@ -203,13 +203,13 @@ window.onload = function () {pageLoad();setSynopsis("mini_PatternSyns.html& >(:<->)</a > :: <span class="keyword" >forall</span - > t t. t -> t -> (<a href="#" + > t t1. t -> t1 -> (<a href="#" >FooType</a > t, <a href="#" >FooType</a > (<a href="#" >FooType</a - > t)) <a href="#" class="selflink" + > t1)) <a href="#" class="selflink" >#</a ></p ><div class="doc" @@ -261,9 +261,9 @@ window.onload = function () {pageLoad();setSynopsis("mini_PatternSyns.html& >E</a > :: <span class="keyword" >forall</span - > k t t. <a href="#" + > k t t1. <a href="#" >(><)</a - > k t t <a href="#" class="selflink" + > k t t1 <a href="#" class="selflink" >#</a ></p ><div class="doc" |