| MetaCoq.Checker.All.html | -rw-r--r-- | 662 bytes |
| MetaCoq.Checker.Closed.html | -rw-r--r-- | 58.9 KB |
| MetaCoq.Checker.Extraction.html | -rw-r--r-- | 4.4 KB |
| MetaCoq.Checker.Generation.html | -rw-r--r-- | 16.9 KB |
| MetaCoq.Checker.LibHypsNaming.html | -rw-r--r-- | 14.4 KB |
| MetaCoq.Checker.Loader.html | -rw-r--r-- | 668 bytes |
| MetaCoq.Checker.MetaTheory.html | -rw-r--r-- | 2.8 KB |
| MetaCoq.Checker.Normal.html | -rw-r--r-- | 45.1 KB |
| MetaCoq.Checker.Reduction.html | -rw-r--r-- | 41.6 KB |
| MetaCoq.Checker.Retyping.html | -rw-r--r-- | 34.3 KB |
| MetaCoq.Checker.Substitution.html | -rw-r--r-- | 332.4 KB |
| MetaCoq.Checker.Typing.html | -rw-r--r-- | 976.6 KB |
| MetaCoq.Checker.TypingWf.html | -rw-r--r-- | 74.1 KB |
| MetaCoq.Checker.Validity.html | -rw-r--r-- | 6.3 KB |
| MetaCoq.Checker.WcbvEval.html | -rw-r--r-- | 206.1 KB |
| MetaCoq.Checker.Weakening.html | -rw-r--r-- | 215.8 KB |
| MetaCoq.Checker.WeakeningEnv.html | -rw-r--r-- | 148.7 KB |
| MetaCoq.Checker.WfInv.html | -rw-r--r-- | 58.2 KB |
| MetaCoq.Checker.uGraph.html | -rw-r--r-- | 308.4 KB |
| MetaCoq.Checker.wGraph.html | -rw-r--r-- | 300.0 KB |
| MetaCoq.Erasure.EAll.html | -rw-r--r-- | 657 bytes |
| MetaCoq.Erasure.EArities.html | -rw-r--r-- | 89.0 KB |
| MetaCoq.Erasure.EAst.html | -rw-r--r-- | 49.9 KB |
| MetaCoq.Erasure.EAstUtils.html | -rw-r--r-- | 77.7 KB |
| MetaCoq.Erasure.EInduction.html | -rw-r--r-- | 25.4 KB |
| MetaCoq.Erasure.EInversion.html | -rw-r--r-- | 31.1 KB |
| MetaCoq.Erasure.ELiftSubst.html | -rw-r--r-- | 126.4 KB |
| MetaCoq.Erasure.EPretty.html | -rw-r--r-- | 90.6 KB |
| MetaCoq.Erasure.ESubstitution.html | -rw-r--r-- | 78.9 KB |
| MetaCoq.Erasure.ETyping.html | -rw-r--r-- | 35.5 KB |
| MetaCoq.Erasure.EWcbvEval.html | -rw-r--r-- | 80.8 KB |
| MetaCoq.Erasure.EWndEval.html | -rw-r--r-- | 6.4 KB |
| MetaCoq.Erasure.ErasureCorrectness.html | -rw-r--r-- | 115.0 KB |
| MetaCoq.Erasure.ErasureFunction.html | -rw-r--r-- | 187.9 KB |
| MetaCoq.Erasure.Extract.html | -rw-r--r-- | 109.7 KB |
| MetaCoq.Erasure.Extraction.html | -rw-r--r-- | 3.1 KB |
| MetaCoq.Erasure.Loader.html | -rw-r--r-- | 668 bytes |
| MetaCoq.Erasure.Prelim.html | -rw-r--r-- | 110.1 KB |
| MetaCoq.Erasure.SafeErasureFunction.html | -rw-r--r-- | 128.8 KB |
| MetaCoq.Erasure.SafeTemplateErasure.html | -rw-r--r-- | 46.6 KB |
| MetaCoq.PCUIC.Extraction.html | -rw-r--r-- | 6.9 KB |
| MetaCoq.PCUIC.PCUICAdmittedLemmata.html | -rw-r--r-- | 113.1 KB |
| MetaCoq.PCUIC.PCUICAll.html | -rw-r--r-- | 668 bytes |
| MetaCoq.PCUIC.PCUICAlpha.html | -rw-r--r-- | 55.6 KB |
| MetaCoq.PCUIC.PCUICAst.html | -rw-r--r-- | 40.8 KB |
| MetaCoq.PCUIC.PCUICAstUtils.html | -rw-r--r-- | 323.1 KB |
| MetaCoq.PCUIC.PCUICChecker.html | -rw-r--r-- | 35.7 KB |
| MetaCoq.PCUIC.PCUICCheckerCompleteness.html | -rw-r--r-- | 812 bytes |
| MetaCoq.PCUIC.PCUICClosed.html | -rw-r--r-- | 76.8 KB |
| MetaCoq.PCUIC.PCUICConfluence.html | -rw-r--r-- | 360.2 KB |
| MetaCoq.PCUIC.PCUICContextConversion.html | -rw-r--r-- | 145.0 KB |
| MetaCoq.PCUIC.PCUICConversion.html | -rw-r--r-- | 206.6 KB |
| MetaCoq.PCUIC.PCUICCumulativity.html | -rw-r--r-- | 81.8 KB |
| MetaCoq.PCUIC.PCUICElimination.html | -rw-r--r-- | 87.3 KB |
| MetaCoq.PCUIC.PCUICEquality.html | -rw-r--r-- | 263.7 KB |
| MetaCoq.PCUIC.PCUICErasedTerm.html | -rw-r--r-- | 5.3 KB |
| MetaCoq.PCUIC.PCUICGeneration.html | -rw-r--r-- | 20.0 KB |
| MetaCoq.PCUIC.PCUICInduction.html | -rw-r--r-- | 68.7 KB |
| MetaCoq.PCUIC.PCUICInversion.html | -rw-r--r-- | 111.3 KB |
| MetaCoq.PCUIC.PCUICLiftSubst.html | -rw-r--r-- | 412.9 KB |
| MetaCoq.PCUIC.PCUICLoader.html | -rw-r--r-- | 674 bytes |
| MetaCoq.PCUIC.PCUICMetaTheory.html | -rw-r--r-- | 6.3 KB |
| MetaCoq.PCUIC.PCUICNameless.html | -rw-r--r-- | 149.6 KB |
| MetaCoq.PCUIC.PCUICNormal.html | -rw-r--r-- | 60.2 KB |
| MetaCoq.PCUIC.PCUICParallelReduction.html | -rw-r--r-- | 683.6 KB |
| MetaCoq.PCUIC.PCUICParallelReductionConfluence.html | -rw-r--r-- | 1.2 MB |
| MetaCoq.PCUIC.PCUICPosition.html | -rw-r--r-- | 196.8 KB |
| MetaCoq.PCUIC.PCUICPretty.html | -rw-r--r-- | 105.6 KB |
| MetaCoq.PCUIC.PCUICPrincipality.html | -rw-r--r-- | 95.7 KB |
| MetaCoq.PCUIC.PCUICReduction.html | -rw-r--r-- | 257.7 KB |
| MetaCoq.PCUIC.PCUICReflect.html | -rw-r--r-- | 56.6 KB |
| MetaCoq.PCUIC.PCUICRetyping.html | -rw-r--r-- | 55.5 KB |
| MetaCoq.PCUIC.PCUICSN.html | -rw-r--r-- | 53.6 KB |
| MetaCoq.PCUIC.PCUICSR.html | -rw-r--r-- | 78.8 KB |
| MetaCoq.PCUIC.PCUICSafeLemmata.html | -rw-r--r-- | 296.4 KB |
| MetaCoq.PCUIC.PCUICSigmaCalculus.html | -rw-r--r-- | 243.4 KB |
| MetaCoq.PCUIC.PCUICSize.html | -rw-r--r-- | 47.6 KB |
| MetaCoq.PCUIC.PCUICSubstitution.html | -rw-r--r-- | 386.0 KB |
| MetaCoq.PCUIC.PCUICTyping.html | -rw-r--r-- | 929.0 KB |
| MetaCoq.PCUIC.PCUICUnivSubst.html | -rw-r--r-- | 58.1 KB |
| MetaCoq.PCUIC.PCUICUnivSubstitution.html | -rw-r--r-- | 239.7 KB |
| MetaCoq.PCUIC.PCUICValidity.html | -rw-r--r-- | 38.3 KB |
| MetaCoq.PCUIC.PCUICWcbvEval.html | -rw-r--r-- | 210.8 KB |
| MetaCoq.PCUIC.PCUICWeakening.html | -rw-r--r-- | 173.7 KB |
| MetaCoq.PCUIC.PCUICWeakeningEnv.html | -rw-r--r-- | 169.6 KB |
| MetaCoq.PCUIC.Pretty.html | -rw-r--r-- | 41.7 KB |
| MetaCoq.PCUIC.TemplateToPCUIC.html | -rw-r--r-- | 35.9 KB |
| MetaCoq.PCUIC.TemplateToPCUICCorrectness.html | -rw-r--r-- | 162.0 KB |
| MetaCoq.SafeChecker.Extraction.html | -rw-r--r-- | 3.5 KB |
| MetaCoq.SafeChecker.Loader.html | -rw-r--r-- | 676 bytes |
| MetaCoq.SafeChecker.PCUICSafeChecker.html | -rw-r--r-- | 521.5 KB |
| MetaCoq.SafeChecker.PCUICSafeConversion.html | -rw-r--r-- | 543.3 KB |
| MetaCoq.SafeChecker.PCUICSafeReduce.html | -rw-r--r-- | 246.2 KB |
| MetaCoq.SafeChecker.PCUICSafeRetyping.html | -rw-r--r-- | 90.7 KB |
| MetaCoq.SafeChecker.SafeTemplateChecker.html | -rw-r--r-- | 51.5 KB |
| MetaCoq.Template.All.html | -rw-r--r-- | 1.3 KB |
| MetaCoq.Template.Ast.html | -rw-r--r-- | 68.5 KB |
| MetaCoq.Template.AstUtils.html | -rw-r--r-- | 285.8 KB |
| MetaCoq.Template.BasicAst.html | -rw-r--r-- | 8.9 KB |
| MetaCoq.Template.ExtractableLoader.html | -rw-r--r-- | 692 bytes |
| MetaCoq.Template.Extraction.html | -rw-r--r-- | 3.3 KB |
| MetaCoq.Template.Induction.html | -rw-r--r-- | 75.1 KB |
| MetaCoq.Template.LiftSubst.html | -rw-r--r-- | 162.5 KB |
| MetaCoq.Template.Loader.html | -rw-r--r-- | 670 bytes |
| MetaCoq.Template.Pretty.html | -rw-r--r-- | 124.3 KB |
| MetaCoq.Template.TemplateMonad.html | -rw-r--r-- | 677 bytes |
| MetaCoq.Template.UnivSubst.html | -rw-r--r-- | 70.2 KB |
| MetaCoq.Template.Universes.html | -rw-r--r-- | 179.1 KB |
| MetaCoq.Template.config.html | -rw-r--r-- | 1.6 KB |
| MetaCoq.Template.monad_utils.html | -rw-r--r-- | 37.2 KB |
| MetaCoq.Template.utils.html | -rw-r--r-- | 883.2 KB |
| coqdoc.css | -rw-r--r-- | 5.9 KB |
| index.html | -rw-r--r-- | 1.8 MB |
| toc.html | -rw-r--r-- | 24.5 KB |
