# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-domains base
base-nnp base Naked pointers prohibited in the OCaml heap
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.17.0 The Coq Proof Assistant
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.0 The Coq Proof Assistant, XML protocol server
dune 3.12.2 Fast, portable, and opinionated build system
ocaml 5.1.1 The OCaml compiler (virtual package)
ocaml-base-compiler 5.1.1 Official release 5.1.1
ocaml-config 3 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"
authors: [
"Massachusetts Institute of Technology"
"Kevix"
"SiFive"
]
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "https://github.com/mit-plv/kami"
bug-reports: "https://github.com/mit-plv/kami/issues"
license: "MIT"
build: [
[make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "coq"]
]
install: [make "EXTERNAL_DEPENDENCIES=1" "install"]
depends: [
"coq" {>= "8.15~"}
"coq-riscv" {= "0.0.4"}
]
dev-repo: "git+https://github.com/mit-plv/kami.git"
synopsis: "A work-in-progress language and compiler for verified low-level programming"
tags: ["logpath:kami"]
url {
src: "https://github.com/mit-plv/kami/archive/refs/tags/v0.0.3.tar.gz"
checksum: "sha512=c76f047b4ade255ce22d1a25a702e69a9ae213e50b7cf3f754c32a80e3fb38ec0f4dda6217e9f34176033f6079efb0ab91b74d3e96f377c65f870f03b8d43a9d"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-kami.0.0.3-rv32i coq.8.17.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-kami.0.0.3-rv32i coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-kami.0.0.3-rv32i coq.8.17.0Total: 67 M
../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInl.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FMap.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInl.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInl.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/FifoCorrect.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/InlineFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Word.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Word.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier64.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier32.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/SemFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModularFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider64.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider32.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInl.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Renaming.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Syntax.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FMap.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Decomposition.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/RefinementFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Specialize.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PartialInlineFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier64.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier32.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Semantics.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/StepDet.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider64.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider32.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Wf.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SC.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PartialInlineFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/InlineFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Word.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/SemFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Decomposition.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Syntax.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tactics.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/RefinementFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Semantics.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Specialize.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Renaming.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBoundEx.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDec.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Duplicate.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SC.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBoundEx.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Label.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/CommonTactics.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetch.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/NatLib.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Duplicate.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FMap.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsList.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/FifoCorrect.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ilist.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDec.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModularFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/InlineFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tutorial.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Notations.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/BSyntax.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/StepDet.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/SemFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tactics.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Wf.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PartialInlineFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/NatLib.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBound.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Decomposition.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetch.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Struct.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Indexer.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Btb.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSC.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier64.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Multiplier32.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider64.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Divider32.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringEq.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ListSupport.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Renaming.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Fifo.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/RefinementFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Label.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimBram.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsOT.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Syntax.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/WordSupport.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Specialize.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimFifo.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemAsync.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/OneEltFifo.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/NativeFifo.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/BSyntax.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Synthesize.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsList.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Semantics.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBoundEx.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBound.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Inline.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInv.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/Extraction.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/RegFile.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tactics.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ilist.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/FifoCorrect.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Names.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Duplicate.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ListSupport.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStage.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Substitute.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Indexer.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Reflection.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Nlia.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemTypes.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Concat.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Kami.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSC.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Misc.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson2.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmPeterson1.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulReport.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal2.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulNormal1.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmMatMulInit.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmHanoi.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmGcd.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmFact.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker2.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmDekker1.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBsort.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker3.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker2.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerWorker1.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32/PgmBankerInit.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Notations.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SC.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/WordSupport.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/VectorFacts.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32Pgm.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Fifo.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SimpleFifoCorrect.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Wf.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModularFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Btb.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/InDepthTutorial.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/StepDet.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Synthesize.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimFifo.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Substitute.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/NativeFifo.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/OneEltFifo.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEq.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/VectorFacts.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Struct.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimBram.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Inline.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Label.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSC.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInv.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsOT.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetchDecode.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Notations.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringEq.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStDec.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/NatLib.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/ModuleBound.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ilist.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemAsync.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsList.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcMemCorrect.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FinNotations.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDec.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/CommonTactics.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFetch.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/BSyntax.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tutorial.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEqNat.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDCorrect.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInl.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/CommonTactics.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Indexer.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEq.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Concat.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Reflection.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/RegFile.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFourStDec.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/ListSupport.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/WordSupport.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEqNat.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInl.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringAsOT.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Nlia.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFCorrect.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/BasicLogic.vo../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/Extraction.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Misc.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Tutorial.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInv.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Struct.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringStringAsOT.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/BasicLogic.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Names.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimFifo.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Inline.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Synthesize.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/VectorFacts.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Substitute.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcThreeStInl.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/NativeFifo.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInl.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Btb.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/PrimBram.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/StringEq.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Fifo.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemAsync.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/OneEltFifo.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/Names.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFDInl.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Concat.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ext/Extraction.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemTypes.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInl.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Reflection.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcFInl.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Nlia.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEq.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/DepEqNat.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/RegFile.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/N_Z_nat_conversions.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecSCN.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/Misc.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/SCMMInl.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FinNotations.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/BasicLogic.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/ProcDecInl.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/MemTypes.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Kami.glob../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Ex/IsaRv32PgmExt.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Kami.v../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Kami/Lib/FinNotations.vopam remove -y coq-kami.0.0.3-rv32i