# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.10.0 Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 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.10~"}
"coq-mathcomp-field" {>= "1.10.0"}
"coq-mathcomp-analysis" {(>= "0.2.0" & <= "0.2.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-02-06"
]
url {
http: "https://github.com/affeldt-aist/infotheo/archive/0.0.7.tar.gz"
checksum: "sha512=8cf6f3580a3afd3bb02197f643adb4ea24237e0ee65f1499d32ac15c3cdc775a5e093f833381ddf59f9de4bc08f032960d71e139281ac504093ec547796424e9"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.0.7 coq.8.10.0Dry 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 2h opam install -y --deps-only coq-infotheo.0.0.7 coq.8.10.0opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y -v coq-infotheo.0.0.7 coq.8.10.0Total: 61 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/chap2.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_choice.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/chap2.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_choice.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/proba.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/cinde.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/proba.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_stone.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fsdist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jfdist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jfdist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fdist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fdist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_stone.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/hamming.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/cinde.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/hamming.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/necset.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/types.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/kraft.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/euclid.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/euclid.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/kraft.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Rbigop.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fsdist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/necset.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/pinsker.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/vandermonde.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Rbigop.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/num_occ.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/pinsker.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/dft.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/num_occ.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/types.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/natbin.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/vandermonde.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrR.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/ln_facts.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrR.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/dft.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/ln_facts.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/natbin.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/pproba.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/log_sum.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/logb.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/aep.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/entropy.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrZ.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/divergence.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jensen.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/poly_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_choice.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/logb.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/pproba.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrZ.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_code.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/variation_dist.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/f2.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/log_sum.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.vo../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/proba.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/chap2.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/jtypes.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/aep.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fdist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/convex_stone.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jfdist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/cinde.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/necset.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/entropy.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssr_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/divergence.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/hamming.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrR.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/euclid.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Rbigop.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/poly_ext.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/fsdist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/kraft.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jensen.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/ln_facts.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/bch.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/f2.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/natbin.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/types.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/num_occ.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Reals_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssralg_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/pinsker.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/convex_fdist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/dft.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/vandermonde.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/bigop_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/decoding.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/ssrZ.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/summary.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/logb.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/repcode.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_code.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/typ_seq.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/string_entropy.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/error_exponent.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/grs.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/pproba.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/log_sum.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/variation_dist.glob../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/tanner.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/checksum.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/partition_inequality.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/entropy.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/aep.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/arg_rmax.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/divergence.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/channel_code.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/alternant.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/f2.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/jensen.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/lib/poly_ext.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/source_code.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/probability/variation_dist.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.v../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vopam remove -y coq-infotheo.0.0.7