# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.14.1 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.08.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1 Official release 4.08.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
homepage: "https://github.com/affeldt-aist/infotheo"
dev-repo: "git+https://github.com/affeldt-aist/infotheo.git"
bug-reports: "https://github.com/affeldt-aist/infotheo/issues"
license: "LGPL-2.1-or-later"
synopsis: "Discrete probabilities and information theory for Coq"
description: """
Infotheo is a Coq library for reasoning about discrete probabilities,
information theory, and linear error-correcting codes."""
build: [
[make "-j%{jobs}%" ]
[make "-C" "extraction" "tests"] {with-test}
]
install: [make "install"]
depends: [
"coq" { (>= "8.13" & < "8.15~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-algebra" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-solvable" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-field" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")}
]
tags: [
"keyword:information theory"
"keyword:probability"
"keyword:error-correcting codes"
"keyword:convexity"
"logpath:infotheo"
"date:2022-01-03"
]
authors: [
"Reynald Affeldt, AIST"
"Manabu Hagiwara, Chiba U. (previously AIST)"
"Jonas Senizergues, ENS Cachan (internship at AIST)"
"Jacques Garrigue, Nagoya U."
"Kazuhiko Sakaguchi, Tsukuba U."
"Taku Asai, Nagoya U. (M2)"
"Takafumi Saikawa, Nagoya U."
"Naruomi Obata, Titech (M2)"
]
url {
http: "https://github.com/affeldt-aist/infotheo/archive/0.3.5.tar.gz"
checksum: "sha512=fd70a421ab8a2d506d2328a912621a6d2160c9b0b576a869291772b70d2937066a0b6e471d531d55ed8d5b6e834273412d7f1b1d8a047972894e9a0a86a40695"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.3.5 coq.8.14.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.3.5 coq.8.14.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.3.5 coq.8.14.1Total: 38 M
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/proba.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/chap2.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/proba.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fsdist.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fdist.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/chap2.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_stone.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jfdist.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fdist.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jfdist.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/bayes.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_stone.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/necset.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fsdist.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/hamming.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/hamming.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_equiv.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/kraft.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/necset.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/euclid.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/bayes.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Rbigop.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/types.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Rbigop.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_equiv.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/kraft.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/pinsker.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/num_occ.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrR.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/types.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/vandermonde.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/euclid.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/vandermonde.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/pinsker.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/num_occ.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/graphoid.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrR.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/dft.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/dft.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/natbin.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/natbin.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/ln_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/ln_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/graphoid.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/logb.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/pproba.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/log_sum.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrZ.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/logb.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrZ.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/proba.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/pproba.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/entropy.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/aep.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jensen.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/divergence.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/log_sum.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/chap2.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/poly_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/aep.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/necset.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fdist.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_code.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/variation_dist.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/f2.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_stone.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/fsdist.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/entropy.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jfdist.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrR.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/divergence.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jensen.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/hamming.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Rbigop.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/poly_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/euclid.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/bayes.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/kraft.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/f2.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/convex_equiv.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/ln_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/natbin.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/types.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/num_occ.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/pinsker.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/dft.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/vandermonde.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/ssrZ.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/logb.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/graphoid.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_code.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/pproba.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/variation_dist.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/log_sum.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/entropy.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/aep.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/divergence.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/f2.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/jensen.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/poly_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/source_code.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/probability/variation_dist.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vopam remove -y coq-infotheo.0.3.5