# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
camlp5 7.14 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-perl 2 Virtual package relying on perl
coq 8.9.1 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.08.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1 Official release 4.08.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Hugo.Herbelin@inria.fr"
homepage: "https://github.com/coq-contribs/lin-alg"
license: "LGPL 2.1"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/LinAlg"]
depends: [
"ocaml"
"coq" {>= "8.9" & < "8.10~"}
"coq-algebra" {>= "8.9" & < "8.10~"}
]
tags: [
"keyword: linear algebra"
"category: Mathematics/Algebra"
"date: 19 spetember 2003"
]
authors: [
"Jasper Stein <jasper@cs.kun.nl>"
]
bug-reports: "https://github.com/coq-contribs/lin-alg/issues"
dev-repo: "git+https://github.com/coq-contribs/lin-alg.git"
synopsis: "Linear Algebra"
description: """
A development of some preliminary linear algebra
based on Chapter 1 of "Linear Algebra" by Friedberg, Insel and Spence"""
flags: light-uninstall
url {
src: "https://github.com/coq-contribs/lin-alg/archive/v8.9.0.tar.gz"
checksum: "md5=91ad67b59d2e256a95f4a9426a353e32"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-lin-alg.8.9.0 coq.8.9.1Dry 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 4h opam install -y --deps-only coq-lin-alg.8.9.0 coq.8.9.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-lin-alg.8.9.0 coq.8.9.1Total: 6 M
../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/spans.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/counting_elements.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/has_n_elements.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrices.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/counting_elements.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/conshdtl.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/finite_misc.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/random_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite_subsets.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/modify_seq.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map_embed.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Equality_structures.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/pointwise.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/restrict.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/has_n_elements.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/before_after.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums2.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/spans.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_facts.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/subseqs.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/empty.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/random_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/const.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/conshdtl.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_seq.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums2.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/counting_elements.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/algebra_omissions.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/arb_intersections.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/pointwise.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite_subsets.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/arb_intersections.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/before_after.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrices.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/has_n_elements.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map2.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map_embed.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/modify_seq.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_facts.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/algebra_omissions.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/spans.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Equality_structures.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/conshdtl.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/finite_misc.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/ring_module.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite_subsets.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/arb_intersections.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/random_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map2.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/subseqs.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/algebra_omissions.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/restrict.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/ring_module.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/omit.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums2.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrices.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/pointwise.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_equality.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map_embed.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/concat.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/modify_seq.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/first_page.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/finite.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/before_after.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/finite_misc.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/more_syntax.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/Map2.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Equality_structures.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/sums.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/const.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/restrict.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/empty.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/ring_module.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/subseqs.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/more_syntax.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/empty.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/const.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/equal_syntax.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/distinct.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_seq.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/seq_set_seq.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/equal_syntax.v../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/first_page.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/more_syntax.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/support/equal_syntax.glob../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/LinAlg/first_page.globopam remove -y coq-lin-alg.8.9.0