# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.15.0 Formal proof management system dune 3.4.1 Fast, portable, and opinionated build system ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" maintainer: "matthieu.sozeau@inria.fr" homepage: "https://metacoq.github.io/metacoq" dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.15" bug-reports: "https://github.com/MetaCoq/metacoq/issues" authors: ["Abhishek Anand <aa755@cs.cornell.edu>" "Danil Annenkov <danil.v.annenkov@gmail.com>" "Simon Boulier <simon.boulier@inria.fr>" "Cyril Cohen <cyril.cohen@inria.fr>" "Yannick Forster <forster@ps.uni-saarland.de>" "Fabian Kunze <fkunze@fakusb.de>" "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>" "Kenji Maillard <kenji.maillard@inria.fr>" "Gregory Malecha <gmalecha@gmail.com>" "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>" "Matthieu Sozeau <matthieu.sozeau@inria.fr>" "Nicolas Tabareau <nicolas.tabareau@inria.fr>" "ThΓ©o Winterhalter <theo.winterhalter@inria.fr>" ] license: "MIT" build: [ ["bash" "./configure.sh"] [make "-j" "%{jobs}%" "-C" "pcuic"] ] install: [ [make "-C" "pcuic" "install"] ] depends: [ "coq-metacoq-template" {= version} ] synopsis: "A type system equivalent to Coq's and its metatheory" description: """ MetaCoq is a meta-programming framework for Coq. The PCUIC module provides a cleaned-up specification of Coq's typing algorithm along with a certified typechecker for it. This module includes the standard metatheory of PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here. """ url { src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.15.tar.gz" checksum: "sha512=83d6b109217139640a081a9ef98b35cf33b1f568b8941f0b23d43abd25d22331cee16fbdd77335583fe74fea0f28215facf1cd9cb416e460a785c6061a454bae" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-metacoq-pcuic.1.1.1+8.15 coq.8.15.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-metacoq-pcuic.1.1.1+8.15 coq.8.15.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-metacoq-pcuic.1.1.1+8.15 coq.8.15.0
Total: 80 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConversion.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLetsCorrectness.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReductionConfluence.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplateCorrectness.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEquality.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICNormal.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICCorrectness.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConfluence.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICPosition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSR.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductiveInversion.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSpine.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReduction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICInstConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLetsCorrectness.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductiveInversion.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICRenameTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICArities.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICWcbvEval.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReductionConfluence.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTyping.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWellScopedCumulativity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductives.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICInstTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConversion.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConfluence.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInduction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWcbvEval.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulProp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSR.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReduction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAlpha.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICNamelessConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSpine.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICUnivSubstitutionConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICCorrectness.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConvCumInversion.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICRenameConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSubstitution.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICDepth.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductives.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICReduction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICOnFreeVars.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICPrincipality.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSigmaCalculus.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICLiftSubst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICReflect.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICInstConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICClosedTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplateCorrectness.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCanonicity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSigmaCalculus.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICUnivSubstitutionTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICAstUtils.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgress.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInversion.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICReduction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTyping.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICUnivSubstitutionConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSubstitution.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWfUniverses.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICOnFreeVars.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextConversion.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICFirstorder.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICElimination.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICClosed.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSafeLemmata.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDTyping.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDStrengthening.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEtaExpand.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICNormal.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDUnique.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContexts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextConversion.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningEnvConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEquality.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgress.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICRenameConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICPosition.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativitySpec.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulProp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningEnvTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICNamelessConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICViews.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLetsCorrectness.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCanonicity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativitySpec.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICLiftSubst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICClosedTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICOnFreeVarsConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICRenameTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductiveInversion.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICElimination.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDTyping.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICExpanded.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDStrengthening.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWfUniverses.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICAstUtils.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWcbvEval.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReductionConfluence.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDToPCUIC.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICClosed.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAlpha.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICContextConversionTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICValidity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativity.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConversion.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConfluence.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSR.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDFromPCUIC.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSafeLemmata.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextReduction.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContexts.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICArities.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICCorrectness.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSpine.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInduction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPrimitive.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICFirstorder.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICDepth.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICUnivSubstitutionTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConvCumInversion.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextSubst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICUnivSubst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICWcbvEval.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWellScopedCumulativity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICParallelReduction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInductives.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningEnvTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICPrincipality.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEtaExpand.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICInstTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDUnique.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWeakeningEnv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICCases.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICOnOne.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplateCorrectness.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICRedTypeIrrelevance.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCasesContexts.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDToPCUIC.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICCases.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInversion.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICClosedConv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICReduction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPretty.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDFromPCUIC.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICContextConversionTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICUnivSubstitutionConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSubstitution.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSigmaCalculus.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICValidity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSN.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPretty.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICInstConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICUtils.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUIC.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICExpanded.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICReflect.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICNamelessTyp.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextReduction.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWeakeningEnv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGlobalEnv.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTransform.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTyping.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGeneration.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCSubst.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGuardCondition.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEquality.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICNormal.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICPosition.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICOnFreeVars.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningEnvConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextConversion.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICNamelessDef.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLets.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulProp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICNamelessConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativity.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICTactics.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAlpha.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplate.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICOnOne.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCanonicity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInstDef.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWfUniverses.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICRenameTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICAst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgram.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgress.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICSize.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICClosedTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICViews.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWcbvEval.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICElimination.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICRenameDef.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextSubst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICOnFreeVarsConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICRenameConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDStrengthening.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSafeLemmata.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICAstUtils.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUIC.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICUtils.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICPrincipality.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCasesContexts.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICFirstorder.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICClosed.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICLiftSubst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativitySpec.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDTyping.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICNamelessDef.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICArities.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContexts.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICWcbvEval.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICInstTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICClosedConv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInduction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningEnvTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWellScopedCumulativity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICConvCumInversion.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICUnivSubstitutionTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICDepth.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLets.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSN.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICEtaExpand.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICNamelessTyp.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICValidity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplate.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDToPCUIC.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICWeakeningEnv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICCases.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGuardCondition.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGlobalEnv.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICUnivSubst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDFromPCUIC.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUICExpanded.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextReduction.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Bidirectional/BDUnique.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICContextConversionTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICRedTypeIrrelevance.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPrimitive.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPretty.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICInversion.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICReflect.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICNamelessTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInstDef.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTransform.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCumulativity.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCSubst.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICContextSubst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICWeakeningEnvConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICTactics.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICOnOne.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGeneration.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICSN.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICSize.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Typing/PCUICWeakeningTyp.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/TemplateToPCUIC.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICOnFreeVarsConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCasesContexts.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICViews.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Conversion/PCUICClosedConv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgram.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICRenameDef.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICUtils.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICNamelessDef.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICExpandLets.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGlobalEnv.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICRedTypeIrrelevance.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICToTemplate.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICPrimitive.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICUnivSubst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICTransform.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGuardCondition.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICInstDef.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICCSubst.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICTactics.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICProgram.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/PCUICGeneration.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/utils/PCUICSize.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/MetaCoq/PCUIC/Syntax/PCUICRenameDef.v
opam remove -y coq-metacoq-pcuic.1.1.1+8.15