# 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@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: "GPL-3.0-or-later" authors: [ "Reynald Affeldt" "Manabu Hagiwara" "Jonas Senizergues" "Jacques Garrigue" "Kazuhiko Sakaguchi" "Taku Asai" "Takafumi Saikawa" "Naruomi Obata" "Erik Martin-Dorel" "Ryosuke Obi" "Mitsuharu Yamamoto" ] build: [ [make "-j%{jobs}%"] [make "-C" "extraction" "tests"] {with-test} ] install: [ [make "install"] ] depends: [ "coq" {>= "8.11" & < "8.12~"} "coq-mathcomp-field" {>= "1.11" & < "1.12~"} "coq-mathcomp-analysis" {>= "0.3.1" & < "0.3.3~"} ] synopsis: "Infotheo" description: """ a Coq formalization of information theory and linear error-correcting codes """ tags: [ "category:Computer Science/Data Types and Data Structures" "keyword: information theory" "keyword: probability" "keyword: error-correcting codes" "logpath:infotheo" "date:2020-06-12" ] url { http: "https://github.com/affeldt-aist/infotheo/archive/v0.1.1.tar.gz" checksum: "sha512=58420885549ae2bafbe95d68dc49a6a889ba26c1e536937971c04618461d1c183be4da68ed4ac6012a56877c309d61476d79a148900d5c91d616dca979bb8106" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.1.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.1.1 coq.8.11.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.1.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/ecc_modern/ldpc_algo_proof.vo
../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/probability/convex_choice.glob
../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/probability/proba.glob
../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/probability/cinde.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/probability/proba.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/probability/convex_stone.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/probability/jfdist.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.glob
../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/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/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/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/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/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/ssr_ext.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/probability/necset.glob
../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.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/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/euclid.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/lib/Rbigop.vo
../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/ssr_ext.glob
../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/probability/fsdist.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/lib/euclid.vo
../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/Rbigop.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/num_occ.glob
../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/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/bigop_ext.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/ssrR.glob
../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/lib/bigop_ext.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/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/information_theory/channel.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/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/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/lib/logb.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/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/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/source_coding_fl_converse.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/probability/partition_inequality.vo
../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/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/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/lib/Reals_ext.glob
../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/entropy.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/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/channel_coding_converse.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/lib/binary_entropy_function.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/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/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/information_theory/source_code.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/probability/variation_dist.vo
../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/lib/Ranalysis_ext.glob
../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/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/lib/classical_sets_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/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/probability/necset.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/probability/partition_inequality.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/channel_coding_converse.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/information_theory/aep.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/probability/jfdist.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/ecc_modern/tanner_partition.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/information_theory/channel_coding_direct.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/hamming_code.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/lib/ssr_ext.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/lib/hamming.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/probability/fsdist.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/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/lib/classical_sets_ext.glob
../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/information_theory/channel_code.glob
../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/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/ecc_classic/poly_decoding.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/information_theory/convex_fdist.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/bigop_ext.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/lib/ssrZ.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/information_theory/joint_typ_seq.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/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/typ_seq.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/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/probability/variation_dist.glob
../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/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/probability/partition_inequality.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/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/lib/classical_sets_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/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/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.1.1