« Up

metacoq-quotation 1.2.1+8.18 9 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.18.0      The Coq Proof Assistant
coq-core              8.18.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.18.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.18.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        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#main"
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>"
          "Jason Gross <jgross@mit.edu>"
          "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" "quotation"]
]
install: [
  [make "-C" "quotation" "install"]
]
depends: [
  "coq-metacoq-template" {= version}
  "coq-metacoq-pcuic" {= version}
  "coq-metacoq-template-pcuic" {= version}
]
synopsis: "Gallina quotation functions for Template Coq"
description: """
MetaCoq is a meta-programming framework for Coq.
The Quotation module is geared at providing functions `□T → □□T` for
`□T := Ast.term` (currently implemented) and for `□T := { t : Ast.term
& Σ ;;; [] |- t : T }` (still in the works).  Currently `Ast.term →
Ast.term` and `(Σ ;;; [] |- t : T) → Ast.term` functions are provided
for Template and PCUIC terms, in `MetaCoq.Quotation.ToTemplate.All`
and `MetaCoq.Quotation.ToPCUIC.All`.  Proving well-typedness is still
a work in progress.
Ultimately the goal of this development is to prove that `□` is a lax monoidal
semicomonad (a functor with `cojoin : □T → □□T` that codistributes over `unit`
and `×`), which is sufficient for proving Löb's theorem.
"""
url {
  src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.18.tar.gz"
  checksum: "sha256=dd129826edd22e611f84cdc82f6486fc57343e13c8223ce041a3d0574b6f5262"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-metacoq-quotation.1.2.1+8.18 coq.8.18.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; timeout 4h opam install -y --deps-only coq-metacoq-quotation.1.2.1+8.18 coq.8.18.0
Return code
0
Duration
22 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-metacoq-quotation.1.2.1+8.18 coq.8.18.0
Return code
0
Duration
9 m 0 s

Installation size

Total: 83 M

  • 9 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/EnvironmentTyping/Sig.vo
  • 9 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/MSets.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/MSets.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/EnvironmentTyping.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/EnvironmentTyping.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/FSets.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/FSets.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCMSets/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCMSets/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Typing.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCFSets/Sig.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCFSets/Sig.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Environment/Sig.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Environment/Sig.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Environment.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Environment.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo
  • 647 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.vo
  • 641 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo
  • 518 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICAst.vo
  • 374 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.vo
  • 368 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo
  • 267 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo
  • 266 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo
  • 261 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo
  • 256 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.vo
  • 238 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo
  • 229 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo
  • 228 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICTyping.vo
  • 228 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo
  • 226 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Universes.vo
  • 224 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo
  • 223 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo
  • 223 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo
  • 222 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo
  • 221 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Universes.vo
  • 221 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.vo
  • 218 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo
  • 217 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo
  • 215 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo
  • 213 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.vo
  • 212 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICCumulativitySpec.vo
  • 208 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.vo
  • 207 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo
  • 207 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.vo
  • 204 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.vo
  • 202 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo
  • 201 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo
  • 199 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo
  • 192 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Ast.vo
  • 186 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Init.vo
  • 179 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.vo
  • 170 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Init.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironment/Instances.vo
  • 163 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.vo
  • 162 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo
  • 161 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo
  • 158 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Init.vo
  • 158 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo
  • 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Init.glob
  • 151 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo
  • 148 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Init.glob
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.vo
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICEquality.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Init.vo
  • 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICReduction.vo
  • 139 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/WfAst.vo
  • 136 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations/Type.vo
  • 135 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo
  • 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TermEquality.vo
  • 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICGlobalMaps/Instances.vo
  • 119 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.vo
  • 116 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo
  • 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations/Type.vo
  • 114 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Kernames.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.glob
  • 108 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/EnvironmentTyping/Sig.glob
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Kernames.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Lists.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvTyping/Instances.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.vo
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/CommonUtils.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Lists.vo
  • 93 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/EnvironmentTyping.glob
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/EnvironmentTyping.glob
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/All_Forall.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Syntax/PCUICCases.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/All_Forall.vo
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironmentHelper/Instances.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCOption.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/BasicAst.vo
  • 68 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICLookup/Instances.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/MSets.glob
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TypingWf.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/All.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICPrimitive.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCOption.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICAstUtils.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/BasicAst.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/MSets.glob
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCProd.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/CommonUtils.glob
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/All.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/Instances.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/AstUtils.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Numbers.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICConversion/Instances.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICDeclarationTyping/Instances.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCProd.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/ssr.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Floats.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Instances.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Numbers.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/ssr.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Floats.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Bool.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTerm/Instances.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCList.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ReflectEq.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/bytestring.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICEnvironmentDecide/Instances.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Instances.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Strings.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Instances.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCReflect.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCArith.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/config.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Primitive.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/PCUICConversionParAlgo/Instances.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/PCUICConversionParSpec/Instances.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICTypingDef/Instances.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTermUtils/Instances.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/utils.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICTermDecide/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCUtils.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Bool.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/Instances.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Instances.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCList.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ReflectEq.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/bytestring.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Instances.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Strings.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCReflect.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCArith.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/config.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/utils.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.glob
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/Instances.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Primitive.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Init.glob
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCUtils.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.glob
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Init.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Init.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Init.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICCumulativitySpec.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Typing.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations/Type.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Universes.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/All_Forall.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Universes.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations/Type.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Environment.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/All_Forall.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Environment.glob
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/FSets.glob
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/FSets.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICTyping.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/EnvironmentTyping.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/EnvironmentTyping.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/CommonUtils.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/EnvironmentTyping/Sig.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCOption.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/MSets.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/MSets.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCOption.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TermEquality.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICEquality.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Lists.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Environment/Sig.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Lists.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Environment/Sig.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Equalities/Sig.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Init.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Init.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/Orders/Sig.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Universes.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICAst.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Universes.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCProd.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCProd.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/ssr.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/ssr.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCMSets/Sig.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersAlt/Sig.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCMSets/Sig.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Typing.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Environment.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Environment.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICReduction.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Ast.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/All.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations/Type.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations/Type.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/FSets.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/FSets.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/All.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/BasicAst.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICTyping.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/BasicAst.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/All_Forall.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/All_Forall.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Lists.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Lists.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Kernames.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICCumulativitySpec.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Kernames.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Numbers.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Numbers.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Syntax/PCUICCases.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/WfAst.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICEquality.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICAst.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCOption.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TermEquality.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCOption.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersFacts/Sig.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Environment/Sig.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Environment/Sig.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/PCUICReduction.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICPrimitive.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCFSets/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMap/Instances.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCFSets/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/BasicAst.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/BasicAst.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Ast.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Syntax/PCUICCases.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Bool.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/ssr.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/ssr.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/All.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Bool.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/All.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/Structures/OrdersTac/Sig.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCMSets/Sig.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCMSets/Sig.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare_opt.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompareSpec.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCProd.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/LibHypsNaming.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/ReflectAst.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/UnivSubst.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/LiftSubst.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Induction.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCProd.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare_opt.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompareSpec.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/monad_utils.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCRelations.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCEquality.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Transform.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/LibHypsNaming.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPrelude.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCCompare.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCString.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCSquash.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Reflect.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/monad_utils.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCRelations.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCEquality.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Transform.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPred.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPrelude.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCCompare.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Induction.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCString.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCSquash.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Reflect.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPred.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Numbers.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Numbers.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Floats.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Instances.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Floats.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Kernames.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Kernames.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetProperties/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICDeclarationTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironmentHelper/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetInterface/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/bytestring.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/bytestring.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapAVL/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCList.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCList.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCArith.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICTypingDef/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetList/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCArith.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/PCUICConversionParSpec/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/WfAst.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/PCUICConversionParAlgo/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICGlobalMaps/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCReflect.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ReflectEq.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCReflect.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICEnvironmentDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICConversion/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ReflectEq.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICAstUtils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCUtils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/AstUtils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCUtils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICTermDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/AstUtils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapDecide/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICAstUtils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Floats.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Floats.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTermUtils/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICLookup/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Level/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TypingWf.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironment/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Env/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapList/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTerm/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Utils/MCFSets/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Utils/MCFSets/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/bytestring.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/bytestring.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Kername/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Bool.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironmentHelper/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Bool.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Equations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Equations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICDeclarationTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/TypingWf.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Strings.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Strings.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetDecide/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/utils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetFacts/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/PCUICConversionParSpec/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/PCUICConversionParAlgo/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/utils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/PCUICTypingDef/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/UnivConstraint/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICGlobalMaps/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICEnvironmentDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExpr/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapFacts/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/Level/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICConversion/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/Level/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapFact/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/MSets/MSetAVL/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/PCUICTermDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameMapDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTermUtils/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ReflectEq.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ReflectEq.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICEnvironment/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelExprSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICLookup/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/ConstraintSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Primitive.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/config.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Kernames/KernameSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCArith.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Primitive.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/config.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Typing/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCArith.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Common/Universes/LevelSet/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCList.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCList.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/Ast/Env/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICAst/PCUICTerm/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/Coq/FSets/FMapInterface/Sig.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCReflect.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCReflect.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Coq/Strings.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Coq/Strings.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/Instances.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCUtils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCUtils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/utils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/config.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/config.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/utils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/Syntax/PCUICReflect/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Primitive.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Primitive.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICTyping/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/QuotationOf/Template/ReflectAst/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativitySpec/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/QuotationOf/PCUIC/PCUICCumulativity/Instances.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare_opt.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompareSpec.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/LibHypsNaming.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/ReflectAst.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/UnivSubst.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/LiftSubst.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Induction.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare_opt.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompareSpec.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/monad_utils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCRelations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCEquality.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Transform.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/LibHypsNaming.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPrelude.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCCompare.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCString.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCSquash.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Reflect.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/monad_utils.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCRelations.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCEquality.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Transform.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPred.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPrelude.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCCompare.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Induction.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCString.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCSquash.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Reflect.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPred.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/monad_utils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/monad_utils.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/UnivSubst.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/ReflectAst.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/LiftSubst.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Template/Induction.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Transform.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Common/Reflect.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/PCUIC/Induction.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Transform.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Common/Reflect.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCString.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCRelations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPrelude.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCPred.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCEquality.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCCompare.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/LibHypsNaming.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare_opt.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompareSpec.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/ByteCompare.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCString.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCRelations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPrelude.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCPred.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCEquality.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCCompare.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/LibHypsNaming.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare_opt.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompareSpec.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/ByteCompare.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/MCSquash.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/MCSquash.v

Uninstall 🧹

Command
opam remove -y coq-metacoq-quotation.1.2.1+8.18
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣