Commit 68988484 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove derived coqdocjs folder.

parent 98d71334
Copyright (c) 2016, Tobias Tebbi
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
var coqdocjs = coqdocjs || {};
coqdocjs.repl = {
"forall": "",
"exists": "",
"~": "¬",
"/\\": "",
"\\/": "",
"->": "",
"<-": "",
"<->": "",
"=>": "",
"<>": "",
"<=": "",
">=": "",
"el": "",
"nel": "",
"<<=": "",
"|-": "",
">>": "»",
"<<": "",
"++": "",
"===": "",
"=/=": "",
"=~=": "",
"==>": "",
"lhd": "",
"rhd": "",
"nat": "",
"alpha": "α",
"beta": "β",
"gamma": "γ",
"delta": "δ",
"epsilon": "ε",
"eta": "η",
"iota": "ι",
"kappa": "κ",
"lambda": "λ",
"mu": "μ",
"nu": "ν",
"omega": "ω",
"phi": "ϕ",
"pi": "π",
"psi": "ψ",
"rho": "ρ",
"sigma": "σ",
"tau": "τ",
"theta": "θ",
"xi": "ξ",
"zeta": "ζ",
"Delta": "Δ",
"Gamma": "Γ",
"Pi": "Π",
"Sigma": "Σ",
"Omega": "Ω",
"Xi": "Ξ"
};
coqdocjs.subscr = {
"0" : "",
"1" : "",
"2" : "",
"3" : "",
"4" : "",
"5" : "",
"6" : "",
"7" : "",
"8" : "",
"9" : "",
};
coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
body{
font-family: 'Open Sans', sans-serif;
font-size: 14px;
color: #2D2D2D
}
a {
text-decoration: none;
border-radius: 3px;
padding-left: 3px;
padding-right: 3px;
margin-left: -3px;
margin-right: -3px;
color: inherit;
font-weight: bold;
}
#main .code a, #main .inlinecode a, #toc a {
font-weight: inherit;
}
a[href]:hover, [clickable]:hover{
background-color: rgba(0,0,0,0.1);
cursor: pointer;
}
h, h1, h2, h3, h4, h5 {
line-height: 1;
color: black;
text-rendering: optimizeLegibility;
font-weight: normal;
letter-spacing: 0.1em;
text-align: left;
}
div + br {
display: none;
}
div:empty{ display: none;}
#main h1 {
font-size: 2em;
}
#main h2 {
font-size: 1.667rem;
}
#main h3 {
font-size: 1.333em;
}
#main h4, #main h5, #main h6 {
font-size: 1em;
}
#toc h2 {
padding-bottom: 0;
}
#main .doc {
margin: 0;
text-align: justify;
}
.inlinecode, .code, #main pre {
font-family: monospace;
}
.code > br:first-child {
display: none;
}
.doc + .code{
margin-top:0.5em;
}
.block{
display: block;
margin-top: 5px;
margin-bottom: 5px;
padding: 10px;
text-align: center;
}
.block img{
margin: 15px;
}
table.infrule {
border: 0px;
margin-left: 50px;
margin-top: 10px;
margin-bottom: 10px;
}
td.infrule {
font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
text-align: center;
padding: 0;
line-height: 1;
}
tr.infrulemiddle hr {
margin: 1px 0 1px 0;
}
.infrulenamecol {
color: rgb(60%,60%,60%);
padding-left: 1em;
padding-bottom: 0.1em
}
.id[type="constructor"], .id[type="projection"], .id[type="method"],
.id[title="constructor"], .id[title="projection"], .id[title="method"] {
color: #A30E16;
}
.id[type="var"], .id[type="variable"],
.id[title="var"], .id[title="variable"] {
color: inherit;
}
.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
color: #A6650F;
}
.id[type="lemma"],
.id[title="lemma"]{
color: #188B0C;
}
.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
color : #2874AE;
}
.comment {
color: #808080;
}
/* TOC */
#toc h2{
letter-spacing: 0;
font-size: 1.333em;
}
/* Index */
#index {
margin: 0;
padding: 0;
width: 100%;
}
#index #frontispiece {
margin: 1em auto;
padding: 1em;
width: 60%;
}
.booktitle { font-size : 140% }
.authors { font-size : 90%;
line-height: 115%; }
.moreauthors { font-size : 60% }
#index #entrance {
text-align: center;
}
#index #entrance .spacer {
margin: 0 30px 0 30px;
}
ul.doclist {
margin-top: 0em;
margin-bottom: 0em;
}
#toc > * {
clear: both;
}
#toc > a {
display: block;
float: left;
margin-top: 1em;
}
#toc a h2{
display: inline;
}
/* replace unicode */
.id[repl] .hidden {
font-size: 0;
}
.id[repl]:before{
content: attr(repl);
}
/* folding proofs */
@keyframes show-proof {
0% {
max-height: 1.2em;
opacity: 1;
}
99% {
max-height: 1000em;
}
100%{
}
}
@keyframes hide-proof {
from {
visibility: visible;
max-height: 10em;
opacity: 1;
}
to {
max-height: 1.2em;
}
}
.proof {
cursor: pointer;
}
.proof * {
cursor: pointer;
}
.proof {
overflow: hidden;
position: relative;
transition: opacity 1s;
display: inline-block;
}
.proof[show="false"] {
max-height: 1.2em;
visibility: visible;
opacity: 0.3;
}
.proof[show="false"][animate] {
animation-name: hide-proof;
animation-duration: 0.25s;
}
.proof[show=true] {
animation-name: show-proof;
animation-duration: 10s;
}
.proof[show="false"]:before {
position: absolute;
visibility: visible;
width: 100%;
height: 100%;
display: block;
opacity: 0;
content: "M";
}
.proof[show="false"]:hover:before {
content: "";
}
.proof[show="false"] + br + br {
display: none;
}
.proof[show="false"]:hover {
visibility: visible;
opacity: 0.5;
}
#toggle-proofs[proof-status="no-proofs"] {
display: none;
}
#toggle-proofs[proof-status="some-hidden"]:before {
content: "Show Proofs";
}
#toggle-proofs[proof-status="all-shown"]:before {
content: "Hide Proofs";
}
/* page layout */
html, body {
height: 100%;
margin:0;
padding:0;
}
@media only screen { /* no div with internal scrolling to allow printing of whole content */
body {
display: flex;
flex-direction: column
}
#content {
flex: 1;
overflow: auto;
display: flex;
flex-direction: column;
}
}
#content:focus {
outline: none; /* prevent glow in OS X */
}
#main {
display: block;
padding: 16px;
padding-top: 1em;
padding-bottom: 2em;
margin-left: auto;
margin-right: auto;
max-width: 60em;
flex: 1 0 auto;
}
.libtitle {
display: none;
}
/* header */
#header {
width:100%;
padding: 0;
margin: 0;
display: flex;
align-items: center;
background-color: rgb(21,57,105);
color: white;
font-weight: bold;
overflow: hidden;
}
.button {
cursor: pointer;
}
#header * {
text-decoration: none;
vertical-align: middle;
margin-left: 15px;
margin-right: 15px;
}
#header > .right, #header > .left {
display: flex;
flex: 1;
align-items: center;
}
#header > .left {
text-align: left;
}
#header > .right {
flex-direction: row-reverse;
}
#header a, #header .button {
color: white;
box-sizing: border-box;
}
#header a {
border-radius: 0;
padding: 0.2em;
}
#header .button {
background-color: rgb(63, 103, 156);
border-radius: 1em;
padding-left: 0.5em;
padding-right: 0.5em;
margin: 0.2em;
}
#header a:hover, #header .button:hover {
background-color: rgb(181, 213, 255);
color: black;
}
#header h1 { padding: 0;
margin: 0;}
/* footer */
#footer {
text-align: center;
opacity: 0.5;
font-size: 75%;
}
/* hyperlinks */
@keyframes highlight {
50%{
background-color: black;
}
}
:target * {
animation-name: highlight;
animation-duration: 1s;
}
a[name]:empty {
float: right;
}
/* Proviola */
div.code {
width: auto;
float: none;
}
div.goal {
position: fixed;
left: 75%;
width: 25%;
top: 3em;
}
div.doc {
clear: both;
}
span.command:hover {
background-color: inherit;
}
var coqdocjs = coqdocjs || {};
(function(){
function replace(s){
var m;
if (m = s.match(/^(.+)'/)) {
return replace(m[1])+"'";
} else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
return replace(m[1])+m[2].replace(/\d/g, function(d){
if (coqdocjs.subscr.hasOwnProperty(d)) {
return coqdocjs.subscr[d];
} else {
return d;
}
});
} else if (coqdocjs.repl.hasOwnProperty(s)){
return coqdocjs.repl[s]
} else {
return s;
}
}
function toArray(nl){
return Array.prototype.slice.call(nl);
}
function replInTextNodes() {
coqdocjs.replInText.forEach(function(toReplace){
toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){
toArray(elem.childNodes).forEach(function(node){
if (node.nodeType != Node.TEXT_NODE) return;
var fragments = node.textContent.split(toReplace);
node.textContent = fragments[fragments.length-1];
for (var k = 0; k < fragments