| MetaCoq.Extraction.EAll.html | -rw-r--r-- | 663 bytes |
| MetaCoq.Extraction.EArities.html | -rw-r--r-- | 89.9 KB |
| MetaCoq.Extraction.EAst.html | -rw-r--r-- | 49.8 KB |
| MetaCoq.Extraction.EAstUtils.html | -rw-r--r-- | 3.1 KB |
| MetaCoq.Extraction.EInduction.html | -rw-r--r-- | 25.7 KB |
| MetaCoq.Extraction.EInversion.html | -rw-r--r-- | 30.1 KB |
| MetaCoq.Extraction.ELiftSubst.html | -rw-r--r-- | 128.3 KB |
| MetaCoq.Extraction.ESubstitution.html | -rw-r--r-- | 79.9 KB |
| MetaCoq.Extraction.ETyping.html | -rw-r--r-- | 35.8 KB |
| MetaCoq.Extraction.EWcbvEval.html | -rw-r--r-- | 142.0 KB |
| MetaCoq.Extraction.EWndEval.html | -rw-r--r-- | 6.5 KB |
| MetaCoq.Extraction.ErasureFunction.html | -rw-r--r-- | 140.2 KB |
| MetaCoq.Extraction.Extract.html | -rw-r--r-- | 110.4 KB |
| MetaCoq.Extraction.Extraction.html | -rw-r--r-- | 2.9 KB |
| MetaCoq.Extraction.ExtractionCorrectness.html | -rw-r--r-- | 74.1 KB |
| MetaCoq.Extraction.Prelim.html | -rw-r--r-- | 115.0 KB |
| MetaCoq.PCUIC.Extraction.html | -rw-r--r-- | 5.8 KB |
| MetaCoq.PCUIC.PCUICAdmittedLemmata.html | -rw-r--r-- | 164.3 KB |
| MetaCoq.PCUIC.PCUICAll.html | -rw-r--r-- | 668 bytes |
| MetaCoq.PCUIC.PCUICAst.html | -rw-r--r-- | 40.4 KB |
| MetaCoq.PCUIC.PCUICAstUtils.html | -rw-r--r-- | 306.2 KB |
| MetaCoq.PCUIC.PCUICChecker.html | -rw-r--r-- | 41.8 KB |
| MetaCoq.PCUIC.PCUICCheckerCompleteness.html | -rw-r--r-- | 812 bytes |
| MetaCoq.PCUIC.PCUICClosed.html | -rw-r--r-- | 69.9 KB |
| MetaCoq.PCUIC.PCUICConfluence.html | -rw-r--r-- | 308.7 KB |
| MetaCoq.PCUIC.PCUICCumulativity.html | -rw-r--r-- | 167.3 KB |
| MetaCoq.PCUIC.PCUICElimination.html | -rw-r--r-- | 73.5 KB |
| MetaCoq.PCUIC.PCUICEquality.html | -rw-r--r-- | 198.1 KB |
| MetaCoq.PCUIC.PCUICErasedTerm.html | -rw-r--r-- | 5.3 KB |
| MetaCoq.PCUIC.PCUICGeneration.html | -rw-r--r-- | 19.9 KB |
| MetaCoq.PCUIC.PCUICInduction.html | -rw-r--r-- | 68.7 KB |
| MetaCoq.PCUIC.PCUICInversion.html | -rw-r--r-- | 108.6 KB |
| MetaCoq.PCUIC.PCUICLiftSubst.html | -rw-r--r-- | 380.5 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-- | 98.1 KB |
| MetaCoq.PCUIC.PCUICNormal.html | -rw-r--r-- | 60.2 KB |
| MetaCoq.PCUIC.PCUICParallelReduction.html | -rw-r--r-- | 748.0 KB |
| MetaCoq.PCUIC.PCUICParallelReductionConfluence.html | -rw-r--r-- | 1.2 MB |
| MetaCoq.PCUIC.PCUICPosition.html | -rw-r--r-- | 192.3 KB |
| MetaCoq.PCUIC.PCUICPrincipality.html | -rw-r--r-- | 107.6 KB |
| MetaCoq.PCUIC.PCUICReduction.html | -rw-r--r-- | 260.7 KB |
| MetaCoq.PCUIC.PCUICReflect.html | -rw-r--r-- | 48.6 KB |
| MetaCoq.PCUIC.PCUICRetyping.html | -rw-r--r-- | 50.5 KB |
| MetaCoq.PCUIC.PCUICSR.html | -rw-r--r-- | 187.1 KB |
| MetaCoq.PCUIC.PCUICSafeLemmata.html | -rw-r--r-- | 314.5 KB |
| MetaCoq.PCUIC.PCUICSubstitution.html | -rw-r--r-- | 372.8 KB |
| MetaCoq.PCUIC.PCUICTyping.html | -rw-r--r-- | 939.6 KB |
| MetaCoq.PCUIC.PCUICUnivSubst.html | -rw-r--r-- | 61.1 KB |
| MetaCoq.PCUIC.PCUICUnivSubstitution.html | -rw-r--r-- | 64.0 KB |
| MetaCoq.PCUIC.PCUICValidity.html | -rw-r--r-- | 33.9 KB |
| MetaCoq.PCUIC.PCUICWcbvEval.html | -rw-r--r-- | 139.0 KB |
| MetaCoq.PCUIC.PCUICWeakening.html | -rw-r--r-- | 211.0 KB |
| MetaCoq.PCUIC.PCUICWeakeningEnv.html | -rw-r--r-- | 143.8 KB |
| MetaCoq.PCUIC.TemplateToPCUIC.html | -rw-r--r-- | 36.3 KB |
| MetaCoq.PCUIC.TemplateToPCUICCorrectness.html | -rw-r--r-- | 159.8 KB |
| MetaCoq.SafeChecker.Extraction.html | -rw-r--r-- | 2.6 KB |
| MetaCoq.SafeChecker.Loader.html | -rw-r--r-- | 676 bytes |
| MetaCoq.SafeChecker.PCUICSafeChecker.html | -rw-r--r-- | 424.8 KB |
| MetaCoq.SafeChecker.PCUICSafeConversion.html | -rw-r--r-- | 460.1 KB |
| MetaCoq.SafeChecker.PCUICSafeReduce.html | -rw-r--r-- | 264.2 KB |
| MetaCoq.Template.All.html | -rw-r--r-- | 1.3 KB |
| MetaCoq.Template.Ast.html | -rw-r--r-- | 68.1 KB |
| MetaCoq.Template.AstUtils.html | -rw-r--r-- | 239.5 KB |
| MetaCoq.Template.BasicAst.html | -rw-r--r-- | 8.9 KB |
| MetaCoq.Template.Closed.html | -rw-r--r-- | 59.1 KB |
| MetaCoq.Template.Extraction.html | -rw-r--r-- | 2.7 KB |
| MetaCoq.Template.Generation.html | -rw-r--r-- | 17.0 KB |
| MetaCoq.Template.Induction.html | -rw-r--r-- | 75.1 KB |
| MetaCoq.Template.LibHypsNaming.html | -rw-r--r-- | 14.4 KB |
| MetaCoq.Template.LiftSubst.html | -rw-r--r-- | 162.5 KB |
| MetaCoq.Template.Loader.html | -rw-r--r-- | 670 bytes |
| MetaCoq.Template.MetaTheory.html | -rw-r--r-- | 2.8 KB |
| MetaCoq.Template.Normal.html | -rw-r--r-- | 45.3 KB |
| MetaCoq.Template.Reduction.html | -rw-r--r-- | 41.6 KB |
| MetaCoq.Template.Retyping.html | -rw-r--r-- | 34.4 KB |
| MetaCoq.Template.Substitution.html | -rw-r--r-- | 333.7 KB |
| MetaCoq.Template.TemplateMonad.Common.html | -rw-r--r-- | 13.4 KB |
| MetaCoq.Template.TemplateMonad.Core.html | -rw-r--r-- | 35.0 KB |
| MetaCoq.Template.TemplateMonad.Extractable.html | -rw-r--r-- | 33.4 KB |
| MetaCoq.Template.TemplateMonad.Monad.html | -rw-r--r-- | 2.9 KB |
| MetaCoq.Template.TemplateMonad.html | -rw-r--r-- | 677 bytes |
| MetaCoq.Template.Typing.html | -rw-r--r-- | 985.1 KB |
| MetaCoq.Template.TypingWf.html | -rw-r--r-- | 74.3 KB |
| MetaCoq.Template.UnivSubst.html | -rw-r--r-- | 72.6 KB |
| MetaCoq.Template.Universes.html | -rw-r--r-- | 158.6 KB |
| MetaCoq.Template.Validity.html | -rw-r--r-- | 6.3 KB |
| MetaCoq.Template.WcbvEval.html | -rw-r--r-- | 149.1 KB |
| MetaCoq.Template.Weakening.html | -rw-r--r-- | 216.6 KB |
| MetaCoq.Template.WeakeningEnv.html | -rw-r--r-- | 135.3 KB |
| MetaCoq.Template.WfInv.html | -rw-r--r-- | 14.4 KB |
| MetaCoq.Template.config.html | -rw-r--r-- | 1.6 KB |
| MetaCoq.Template.kernel.Checker.html | -rw-r--r-- | 533.8 KB |
| MetaCoq.Template.monad_utils.html | -rw-r--r-- | 37.2 KB |
| MetaCoq.Template.uGraph.html | -rw-r--r-- | 313.3 KB |
| MetaCoq.Template.utils.html | -rw-r--r-- | 733.3 KB |
| MetaCoq.Template.wGraph.html | -rw-r--r-- | 301.3 KB |
| coqdoc.css | -rw-r--r-- | 5.7 KB |
| index.html | -rw-r--r-- | 1.6 MB |
| toc.html | -rw-r--r-- | 22.7 KB |
