Deploying to gh-pages from @ 53fff5a 🚀

Mcltt.Algorithmic.Subtyping.Definitions.html

@@ -28,9 +28,9 @@
 <h1 class="libtitle">Mcltt.Algorithmic.Subtyping.Definitions</h1>
 
 <div class="code">
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#"><span class="id" title="library">System.Definitions</span></a> <a class="idref" href="Mcltt.Core.Semantic.NbE.html#"><span class="id" title="library">NbE</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#"><span class="id" title="library">Syntax</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Semantic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Semantic.NbE.html#"><span class="id" title="library">NbE</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.SystemOpt.html#"><span class="id" title="library">SystemOpt</span></a>.<br/>
 <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#Syntax_Notations"><span class="id" title="module">Syntax_Notations</span></a>.<br/>
 
 <br/>

Mcltt.Algorithmic.Subtyping.Lemmas.html

@@ -28,11 +28,11 @@
 <h1 class="libtitle">Mcltt.Algorithmic.Subtyping.Lemmas</h1>
 
 <div class="code">
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.html#"><span class="id" title="library">Evaluation</span></a> <a class="idref" href="Mcltt.Core.Semantic.Readback.html#"><span class="id" title="library">Readback</span></a> <a class="idref" href="Mcltt.Core.Semantic.NbE.html#"><span class="id" title="library">NbE</span></a> <a class="idref" href="Mcltt.Core.Syntactic.CoreTypeInversions.html#"><span class="id" title="library">CoreTypeInversions</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Presup.html#"><span class="id" title="library">Presup</span></a> <a class="idref" href="Mcltt.Core.Syntactic.CtxSub.html#"><span class="id" title="library">CtxSub</span></a> <a class="idref" href="Mcltt.Core.Syntactic.SystemOpt.html#"><span class="id" title="library">SystemOpt</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Completeness</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Completeness.Consequences.Rules.html#"><span class="id" title="library">Consequences.Rules</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Completeness.html#"><span class="id" title="library">Completeness</span></a> <a class="idref" href="Mcltt.Core.Soundness.html#"><span class="id" title="library">Soundness</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Definitions.html#"><span class="id" title="library">Subtyping.Definitions</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Subtyping</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Definitions.html#"><span class="id" title="library">Definitions</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a> <a class="idref" href="Mcltt.Core.Soundness.html#"><span class="id" title="library">Soundness</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.SystemOpt.html#"><span class="id" title="library">SystemOpt</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Completeness.Consequences</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Completeness.Consequences.Rules.html#"><span class="id" title="library">Rules</span></a>.<br/>
 <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#Syntax_Notations"><span class="id" title="module">Syntax_Notations</span></a>.<br/>
 
 <br/>

Mcltt.Core.Syntactic.ExpNoConfusion.html → Mcltt.Algorithmic.Subtyping.html

@@ -25,22 +25,10 @@
 </div>
     <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
     <div id="main">
-<h1 class="libtitle">Mcltt.Core.Syntactic.ExpNoConfusion</h1>
+<h1 class="libtitle">Mcltt.Algorithmic.Subtyping</h1>
 
 <div class="code">
-</div>
-
-<div class="doc">
-For some reason, fitting this file in Syntax.v breaks menhir... Who knows? 
-</div>
-<div class="code">
-
-<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="keyword">Equations</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Equations</span>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#"><span class="id" title="library">Syntax</span></a>.<br/>
-
-<br/>
-<span class="id" title="keyword">Derive</span> <span class="id" title="var">NoConfusion</span> <span class="id" title="keyword">for</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#exp"><span class="id" title="inductive">exp</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#sub"><span class="id" title="inductive">sub</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Subtyping</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Definitions.html#"><span class="id" title="library">Definitions</span></a> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Lemmas.html#"><span class="id" title="library">Lemmas</span></a>.<br/>
 </div>
 </div>
 <div id="footer">

Mcltt.Algorithmic.Typing.Definitions.html

@@ -28,12 +28,8 @@
 <h1 class="libtitle">Mcltt.Algorithmic.Typing.Definitions</h1>
 
 <div class="code">
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Definitions.html#"><span class="id" title="library">Subtyping.Definitions</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Soundness.html#"><span class="id" title="library">Soundness</span></a> <a class="idref" href="Mcltt.Core.Completeness.html#"><span class="id" title="library">Completeness</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Semantic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Semantic.NbE.html#"><span class="id" title="library">NbE</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#"><span class="id" title="library">System.Definitions</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#"><span class="id" title="library">Syntax</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Subtyping</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Definitions.html#"><span class="id" title="library">Definitions</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a>.<br/>
 <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#Domain_Notations"><span class="id" title="module">Domain_Notations</span></a>.<br/>
 
 <br/>

Mcltt.Algorithmic.Typing.Lemmas.html

@@ -28,13 +28,12 @@
 <h1 class="libtitle">Mcltt.Algorithmic.Typing.Lemmas</h1>
 
 <div class="code">
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Algorithmic.Typing.Definitions.html#"><span class="id" title="library">Typing.Definitions</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Lemmas.html#"><span class="id" title="library">Subtyping.Lemmas</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Soundness.html#"><span class="id" title="library">Soundness</span></a> <a class="idref" href="Mcltt.Core.Completeness.html#"><span class="id" title="library">Completeness</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.LibTactics.html#"><span class="id" title="library">LibTactics</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Typing</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Algorithmic.Typing.Definitions.html#"><span class="id" title="library">Definitions</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Subtyping</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Subtyping.Lemmas.html#"><span class="id" title="library">Lemmas</span></a>.<br/>
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Base.html#"><span class="id" title="library">Base</span></a>.<br/>
 <span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Completeness</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Completeness.Consequences.Rules.html#"><span class="id" title="library">Consequences.Rules</span></a>.<br/>
 <span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Semantic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Semantic.Consequences.html#"><span class="id" title="library">Consequences</span></a>.<br/>
-<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Core.Syntactic</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Core.Syntactic.SystemOpt.html#"><span class="id" title="library">SystemOpt</span></a>.<br/>
 <span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Frontend</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Frontend.Elaborator.html#"><span class="id" title="library">Elaborator</span></a>.<br/>
 <span class="id" title="keyword">Import</span> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#Domain_Notations"><span class="id" title="module">Domain_Notations</span></a>.<br/>
 

Mcltt.Algorithmic.Typing.html

@@ -0,0 +1,40 @@
+<!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="resources/coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css" />
+<script type="text/javascript" src="resources/config.js"></script>
+<script type="text/javascript" src="resources/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="./dep.html"> Table of Contents </a>
+    </span>
+</div>
+    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
+<h1 class="libtitle">Mcltt.Algorithmic.Typing</h1>
+
+<div class="code">
+<span class="id" title="keyword">From</span> <span class="id" title="var">Mcltt.Algorithmic.Typing</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Mcltt.Algorithmic.Typing.Definitions.html#"><span class="id" title="library">Definitions</span></a> <a class="idref" href="Mcltt.Algorithmic.Typing.Lemmas.html#"><span class="id" title="library">Lemmas</span></a>.<br/>
+</div>
+</div>
+<div id="footer">
+  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/coq-community/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>