# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.17.0 The Coq Proof Assistant
coq-core 8.17.0 The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib 8.17.0 The Coq Proof Assistant -- Standard Library
coqide-server 8.17.0 The Coq Proof Assistant, XML protocol server
dune 3.13.0 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 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.17" & < "8.19~"}
"coq-mathcomp-ssreflect" {>= "1.16.0" & < "1.19~"}
"coq-mathcomp-fingroup"
"coq-mathcomp-algebra"
"coq-mathcomp-solvable"
"coq-mathcomp-field"
"coq-mathcomp-analysis" { (>= "0.5.4") & (< "0.7~")}
"coq-hierarchy-builder" { >= "1.3.0" }
]
tags: [
"keyword:information theory"
"keyword:probability"
"keyword:error-correcting codes"
"keyword:convexity"
"logpath:infotheo"
"date:2023-06-03"
]
authors: [
"Reynald Affeldt, AIST"
"Manabu Hagiwara, Chiba U. (previously AIST)"
"Jonas Senizergues, ENS Cachan (internship at AIST)"
"Jacques Garrigue, Nagoya U."
"Kazuhiko Sakaguchi, Tsukuba U."
"Taku Asai, Nagoya U. (M2)"
"Takafumi Saikawa, Nagoya U."
"Naruomi Obata, Titech (M2)"
]
url {
src: "https://github.com/affeldt-aist/infotheo/archive/0.5.2.tar.gz"
checksum: "sha512=8abf0a7d6782c6fc7d92a4222d3051f6992c5de1541c9ea26f3c11cd87145bf1fee5348791e64b12eeae9fb2aea8c3fdb4e2d8f03dd84556c83a135781dc6c28"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.5.2 coq.8.17.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-infotheo.0.5.2 coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-infotheo.0.5.2 coq.8.17.0Total: 40 M
../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fdist.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/proba.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fsdist.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/proba.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/jtypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/vandermonde.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fdist.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/necset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_stone.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/jtypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/bayes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/repcode.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_stone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/hamming.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/hamming.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fsdist.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssr_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/kraft.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssralg_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssr_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/euclid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Reals_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/necset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/bch.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/bayes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/bch.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Rbigop.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/bigop_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Rbigop.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/types.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_equiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy_convex.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssralg_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Reals_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/num_occ.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrR.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/kraft.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/pproba.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/pinsker.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/types.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/vandermonde.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/euclid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/bigop_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/pinsker.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jfdist_cond.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/num_occ.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrR.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/decoding.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/dft.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jfdist_cond.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/dft.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy_convex.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/graphoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/degree_profile.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/natbin.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/natbin.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/ln_facts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/grs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/ln_facts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/decoding.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/graphoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/grs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/logb.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/repcode.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/error_exponent.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/string_entropy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/log_sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/typ_seq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrZ.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/logb.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/checksum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/error_exponent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/proba.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/partition_inequality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/typ_seq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrZ.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/pproba.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/string_entropy.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/aep.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/checksum.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jensen.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo_proof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/divergence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/log_sum.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_code.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fdist.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/aep.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/subgraph_partition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/poly_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/alternant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/partition_inequality.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/variation_dist.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_code.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/jtypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/f2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/necset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_stone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/fsdist.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner_partition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/linearcode.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_direct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/hamming_code.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Reals_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_converse.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssr_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrR.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/divergence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/reed_solomon.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/hamming.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jensen.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Rbigop.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/poly_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/stopping_set.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/euclid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/bayes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/kraft.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_erasure.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary_tanner.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/f2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_code.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssralg_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/cyclic_code.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/bch.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/convex_equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/ln_facts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/natbin.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/types.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/num_occ.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/alternant.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/bigop_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/pinsker.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/poly_decoding.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/entropy_convex.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/dft.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/vandermonde.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_vl_direct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/ssrZ.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/Ranalysis_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jfdist_cond.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/decoding.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/success_decode_bound.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/summary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/logb.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/repcode.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/joint_typ_seq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/ldpc_algo.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/conditional_divergence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_code.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/graphoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/typ_seq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/error_exponent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/grs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/string_entropy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/pproba.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_converse.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_coding_fl_direct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/variation_dist.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/log_sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/binary_symmetric_channel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/tanner.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/checksum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_coding_converse.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/partition_inequality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/shannon_fano.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/aep.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_modern/max_subset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/binary_entropy_function.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/divergence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/f2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/channel_code.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/alternant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/ecc_classic/mceliece.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/jensen.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/poly_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/conditional_entropy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/erasure_channel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/information_theory/source_code.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/probability/variation_dist.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_ordn.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/lib/classical_sets_ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/infotheo/toy_examples/expected_value_variance_tuple.vopam remove -y coq-infotheo.0.5.2