« Up

lin-alg 8.5.0 5 m 0 s 🏆

Context

# 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.5.3       Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.03.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.03.0      Official 4.03.0 release
ocaml-config        1           OCaml Switch Configuration
# opam file:
opam-version: "2.0"
maintainer: "matej.kosik@inria.fr"
homepage: "https://github.com/coq-contribs/lin-alg"
license: "LGPL 2"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/LinAlg"]
depends: [
  "ocaml"
  "coq" {>= "8.5" & < "8.6~"}
  "coq-algebra" {= "8.5.0"}
]
tags: [ "keyword:linear algebra" "category:Mathematics/Algebra" "date:2003-09-19" ]
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.5.0.tar.gz"
  checksum: "md5=983546bb8f5bde072f900e2e78630aae"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-lin-alg.8.5.0 coq.8.5.3
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-lin-alg.8.5.0 coq.8.5.3
Return code
0
Duration
2 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-lin-alg.8.5.0 coq.8.5.3
Return code
0
Duration
5 m 0 s

Installation size

Total: 6 M

  • 298 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.vo
  • 162 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit.vo
  • 144 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/spans.vo
  • 123 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/counting_elements.vo
  • 115 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.vo
  • 108 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.vo
  • 107 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.vo
  • 102 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.glob
  • 84 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.glob
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.vo
  • 82 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.vo
  • 81 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/has_n_elements.vo
  • 79 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.vo
  • 79 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.vo
  • 78 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit_facts.glob
  • 77 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrices.vo
  • 71 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit_facts.vo
  • 70 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/counting_elements.glob
  • 66 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.vo
  • 66 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.glob
  • 64 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/conshdtl.vo
  • 63 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/finite_misc.vo
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.vo
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.vo
  • 60 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.vo
  • 59 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.vo
  • 59 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.vo
  • 59 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.vo
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.vo
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct_facts.vo
  • 55 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.vo
  • 54 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.vo
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.vo
  • 53 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.vo
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases.vo
  • 50 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/random_facts.vo
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.glob
  • 49 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.glob
  • 47 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.vo
  • 47 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite_subsets.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/modify_seq.vo
  • 45 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Equality_structures.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map_embed.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/pointwise.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/restrict.vo
  • 44 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.vo
  • 42 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/has_n_elements.glob
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/before_after.vo
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums2.vo
  • 40 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.vo
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/spans.glob
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat_facts.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_facts.vo
  • 38 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.glob
  • 36 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums.vo
  • 35 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.glob
  • 35 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.vo
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite.vo
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct_facts.glob
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/subseqs.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.glob
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.vo
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/empty.vo
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/const.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/random_facts.glob
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.glob
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_seq.vo
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.glob
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.glob
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/conshdtl.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat_facts.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums2.glob
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/algebra_omissions.vo
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/counting_elements.v
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.glob
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.glob
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_theorem.v
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dep_facts.v
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/pointwise.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite_subsets.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/arb_intersections.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.glob
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.glob
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/before_after.glob
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrices.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/has_n_elements.v
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map2.vo
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map_embed.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/arb_intersections.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_dim.v
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit_facts.v
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/modify_seq.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_facts.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/algebra_omissions.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/spans.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Equality_structures.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_combinations.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Fn.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_dependence.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct_facts.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/maxlinindepsubsets.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/conshdtl.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality_facts.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/finite_misc.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/direct_sum.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_functionspace.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_between_subsets.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/ring_module.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspaces.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite_subsets.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/arb_intersections.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/random_facts.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map2.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/subseqs.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/algebra_omissions.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/matrix_algebra.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/subspace_bases.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/algebraic_span_facts.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_finite_dim.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/restrict.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/ring_module.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/omit.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/replacement_corollaries.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/vecspace_Mmn.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/alt_build_vecsp.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/mult_by_scalars.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums2.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat_facts.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/Lin_trafos.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrices.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/pointwise.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_equality.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map_embed.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/concat.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/modify_seq.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/first_page.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/bases_from_generating_sets.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/up_lo_triang_mat.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distribution_lemmas.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_facts.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/before_after.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/vecspaces_verybasic.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/finite_misc.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/Matrix_multiplication.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/finite.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/LinAlg/lin_comb_facts.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/trivial_spaces.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/Map2.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Equality_structures.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/more_syntax.vo
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/sums.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/cast_seq_lengths.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/symmetric_matrices.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/const.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Inter_intersection.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/restrict.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/empty.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/ring_module.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/subseqs.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/more_syntax.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/infinite_sequences.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/empty.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/examples/antisymmetric_matrices.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/const.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/distinct.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_seq.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/equal_syntax.vo
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/seq_set_seq.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/extras/Matrix_related_defs.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/equal_syntax.v
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/first_page.vo
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/more_syntax.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/support/equal_syntax.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/LinAlg/first_page.glob

Uninstall 🧹

Command
opam remove -y coq-lin-alg.8.5.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣