# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-num base Num library distributed with the OCaml compiler 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.7.0 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.04.2 The OCaml compiler (virtual package) ocaml-base-compiler 4.04.2 Official 4.04.2 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 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.7" & < "8.8~"} "coq-algebra" {>= "8.7" & < "8.8~"} ] 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.7.0.tar.gz" checksum: "md5=20f96c76f2cd75683420a873349508b1" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-lin-alg.8.7.0 coq.8.7.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-lin-alg.8.7.0 coq.8.7.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-lin-alg.8.7.0 coq.8.7.0
Total: 6 M
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/spans.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/counting_elements.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/has_n_elements.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrices.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/counting_elements.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/conshdtl.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/finite_misc.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/random_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite_subsets.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/modify_seq.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Equality_structures.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map_embed.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/pointwise.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/restrict.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/has_n_elements.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/before_after.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums2.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/spans.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_facts.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/subseqs.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/empty.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/const.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/random_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_seq.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/conshdtl.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums2.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/algebra_omissions.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/counting_elements.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/arb_intersections.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/pointwise.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite_subsets.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/arb_intersections.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/before_after.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrices.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/has_n_elements.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map2.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map_embed.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/modify_seq.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_facts.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/algebra_omissions.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/spans.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Equality_structures.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/conshdtl.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/finite_misc.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/ring_module.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite_subsets.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/arb_intersections.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/random_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map2.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/subseqs.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/algebra_omissions.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/restrict.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/ring_module.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/omit.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums2.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrices.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/pointwise.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_equality.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map_embed.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/concat.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/modify_seq.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/first_page.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/finite.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/before_after.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/finite_misc.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/Map2.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Equality_structures.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/more_syntax.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/sums.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/const.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/restrict.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/empty.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/ring_module.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/subseqs.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/more_syntax.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/empty.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/const.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/distinct.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/equal_syntax.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_seq.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/seq_set_seq.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/equal_syntax.v
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/first_page.vo
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/more_syntax.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/support/equal_syntax.glob
../ocaml-base-compiler.4.04.2/lib/coq/user-contrib/LinAlg/first_page.glob
opam remove -y coq-lin-alg.8.7.0