# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.9.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
# opam file:
opam-version: "2.0"
name: "coq-infotheo"
maintainer: "reynald.affeldt@aist.go.jp"
homepage: "https://github.com/affeldt-aist/infotheo"
bug-reports: "https://github.com/affeldt-aist/infotheo/issues"
dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
license: "GPLv3"
authors: [
"Reynald Affeldt"
"Manabu Hagiwara"
"Jonas Senizergues"
"Jacques Garrigue"
"Kazuhiko Sakaguchi"
"Taku Asai"
"Takafumi Saikawa"
"Naruomi Obata"
"Erik Martin-Dorel"
]
build: [
["coq_makefile" "-f" "_CoqProject" "-o" "Makefile"]
[make]
]
install: [
[make "install"]
]
depends: [
"coq" { (>= "8.9.1" & < "8.10.0~") }
"coq-mathcomp-field" { (>= "1.9.0") & < "1.10.0~"}
"coq-mathcomp-analysis" {(>= "0.2.0" & <= "0.2.2")}
]
synopsis: "Infotheo"
description: """
a Coq formalization of information theory and linear error-correcting codes
"""
url {
http: "https://github.com/affeldt-aist/infotheo/archive/0.0.1.tar.gz"
checksum: "md5=e6afd4e32db51b6bace854f65324b32e"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.0.1 coq.8.9.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-infotheo.0.0.1 coq.8.9.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.0.1 coq.8.9.1Total: 37 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/chap2.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/proba.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/chap2.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/proba.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cinde.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex_stone.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/dist.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex_stone.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/hamming.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cinde.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cproba.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/hamming.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cproba.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/types.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/kraft.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/euclid.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Rbigop.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/euclid.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/kraft.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_dist.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/dist.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/vandermonde.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Rbigop.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/num_occ.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/dft.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/num_occ.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/natbin.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/types.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/vandermonde.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrR.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker_function.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/ln_facts.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrR.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_dist.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/dft.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/ln_facts.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/natbin.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/pproba.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker_function.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/log_sum.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/logb.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/aep.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/entropy.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrZ.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/divergence.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jensen.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/poly_ext.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/proba.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/logb.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/pproba.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrZ.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_code.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/variation_dist.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/f2.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.vo../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/chap2.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/log_sum.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/aep.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex_stone.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/entropy.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cinde.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/divergence.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/hamming.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/poly_ext.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/euclid.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Rbigop.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jensen.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/kraft.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/cproba.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrR.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/ln_facts.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/dist.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/f2.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/types.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/natbin.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/num_occ.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_dist.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/dft.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/vandermonde.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/ssrZ.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker_function.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/logb.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_code.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/pinsker.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/variation_dist.glob../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/log_sum.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/pproba.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/aep.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/entropy.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/divergence.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/f2.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jensen.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/poly_ext.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_code.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.v../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/variation_dist.vopam remove -y coq-infotheo.0.0.1