# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils coq 8.11.0 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.5 A library manager for OCaml # 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.11" & < "8.13~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") } "coq-mathcomp-analysis" { (= "0.3.4") } ] tags: [ "keyword:information theory" "keyword:probability" "keyword:error-correcting codes" "logpath:infotheo" ] 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.2.1.tar.gz" checksum: "sha512=d2374a83ea23283b20572fc91105d9e457869294663c1574d920cc65eb4afbd220a57dffed19d0185f760df47ddf84895fce3aec68f2f8654ea1d2eb8cf46af2" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.2.1 coq.8.11.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.2.1 coq.8.11.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.2.1 coq.8.11.0
Total: 67 M
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.vo
../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/probability/convex_choice.vo
../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/probability/convex_choice.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/probability/proba.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/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/ecc_modern/ldpc_algo_proof.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/information_theory/channel_coding_direct.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/ecc_classic/hamming_code.vo
../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/ecc_modern/tanner_partition.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/probability/fsdist.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/fdist.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/fdist.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.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/repcode.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/ecc_classic/linearcode.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jfdist.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jfdist.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/necset.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/ldpc.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.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/lib/ssr_ext.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/lib/hamming.glob
../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/hamming_code.glob
../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/ecc_classic/bch.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/necset.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.vo
../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_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/information_theory/types.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/lib/ssr_ext.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/fsdist.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/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/information_theory/kraft.vo
../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/lib/euclid.vo
../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/lib/Rbigop.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/bigop_ext.glob
../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/probability/pinsker.glob
../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/lib/ssrR.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/ecc_classic/poly_decoding.glob
../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.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/ecc_classic/decoding.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.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/lib/vandermonde.glob
../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/ecc_classic/cyclic_code.glob
../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/probability/ln_facts.vo
../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_modern/ldpc_algo.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/conditional_divergence.vo
../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/probability/graphoid.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.glob
../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/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/lib/ssralg_ext.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/graphoid.vo
../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/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/binary_symmetric_channel.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/information_theory/string_entropy.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.glob
../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/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/information_theory/typ_seq.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/information_theory/binary_symmetric_channel.glob
../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/ecc_classic/decoding.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/source_coding_fl_converse.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/ecc_modern/summary.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/convex_choice.v
../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/entropy.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/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/information_theory/channel_coding_converse.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/ecc_classic/repcode.glob
../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/lib/binary_entropy_function.vo
../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/jensen.vo
../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/information_theory/channel_code.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/toy_examples/expected_value_variance_ordn.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/toy_examples/expected_value_variance_tuple.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/poly_ext.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/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/probability/proba.v
../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/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/lib/f2.vo
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.glob
../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/ecc_modern/ldpc_algo_proof.v
../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/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/ecc_modern/ldpc_algo.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/subgraph_partition.v
../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/lib/binary_entropy_function.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/necset.v
../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/partition_inequality.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/ecc_modern/tanner.glob
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/fdist.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/lib/classical_sets_ext.vo
../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/ecc_modern/tanner_partition.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_classic/linearcode.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/jfdist.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/hamming_code.v
../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/information_theory/source_coding_vl_converse.v
../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/ecc_modern/max_subset.glob
../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_classic/reed_solomon.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/probability/fsdist.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/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/lib/euclid.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/information_theory/kraft.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/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/toy_examples/expected_value_variance.glob
../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/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/information_theory/channel_code.glob
../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/lib/natbin.v
../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/num_occ.v
../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/lib/Reals_ext.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/ssralg_ext.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/lib/bigop_ext.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.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/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/information_theory/source_coding_vl_direct.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.glob
../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/lib/ssrZ.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/toy_examples/expected_value_variance_ordn.glob
../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/information_theory/success_decode_bound.v
../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/lib/logb.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/probability/graphoid.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/information_theory/joint_typ_seq.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/ecc_modern/ldpc_algo.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.glob
../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/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/ecc_classic/grs.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/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/log_sum.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/probability/variation_dist.glob
../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/information_theory/channel_coding_converse.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/information_theory/shannon_fano.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/probability/partition_inequality.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/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/information_theory/channel_code.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/ecc_classic/mceliece.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/lib/poly_ext.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.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.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.v
../ocaml-base-compiler.4.07.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.v
opam remove -y coq-infotheo.0.2.1