# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.15.0 Formal proof management system dune 3.1.1 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.3 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.14" & < "8.16~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-analysis" { (>= "0.4.0") & (< "0.6~")} ] tags: [ "keyword:information theory" "keyword:probability" "keyword:error-correcting codes" "keyword:convexity" "logpath:infotheo" "date:2022-04-14" ] 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.7.tar.gz" checksum: "sha512=5c49496ea6042c0cfed10c69f3d4ea8c6c6433c574b1d308174792213ed46e28c22d797f8eab5ef2a5e9ad1eeb4bd1fa9f3fc50e392c449a92395a77432a90cd" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.3.7 coq.8.15.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-infotheo.0.3.7 coq.8.15.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.3.7 coq.8.15.0
Total: 37 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/probability/convex.glob
../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.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_modern/subgraph_partition.glob
../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/probability/jfdist.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/fdist.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/reed_solomon.glob
../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/linearcode.vo
../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/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/probability/necset.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/lib/hamming.vo
../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/probability/convex_equiv.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/information_theory/success_decode_bound.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/ecc_modern/tanner_partition.glob
../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/information_theory/kraft.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/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/ecc_modern/summary_tanner.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/probability/bayes.glob
../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_classic/cyclic_code.vo
../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/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/information_theory/types.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/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/information_theory/kraft.vo
../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.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/information_theory/types.glob
../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/bigop_ext.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/euclid.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/lib/ssralg_ext.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/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/num_occ.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/information_theory/source_coding_vl_direct.glob
../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/lib/dft.vo
../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/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/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/ecc_classic/grs.vo
../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/probability/ln_facts.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/information_theory/channel.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/ecc_modern/summary.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/ecc_classic/decoding.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/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/ecc_classic/repcode.glob
../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/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/probability/convex.v
../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/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/information_theory/source_coding_fl_direct.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/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/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/poly_ext.vo
../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/ecc_classic/alternant.vo
../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/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.v
opam remove -y coq-infotheo.0.3.7