# 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 camlp4 4.03+1 Camlp4 is a system for writing extensible parsers for programming languages conf-findutils 1 Virtual package relying on findutils conf-which 1 Virtual package relying on which coq 8.5.0~camlp4 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 ocamlbuild 0.14.2 OCamlbuild is a build system with builtin rules to easily build most OCaml projects # opam file: opam-version: "2.0" maintainer: "matej.kosik@inria.fr" homepage: "https://github.com/coq-contribs/algebra" license: "LGPL 2" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Algebra"] depends: [ "ocaml" "coq" {>= "8.5" & < "8.6~"} ] tags: [ "keyword:algebra" "category:Mathematics/Algebra" "date:1999-03" ] authors: [ "Loรฏc Pottier <>" ] bug-reports: "https://github.com/coq-contribs/algebra/issues" dev-repo: "git+https://github.com/coq-contribs/algebra.git" synopsis: "Basics notions of algebra" flags: light-uninstall url { src: "https://github.com/coq-contribs/algebra/archive/v8.5.0.tar.gz" checksum: "md5=9ef1b5f1f670d56a55aef37d8c511df9" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-algebra.8.5.0 coq.8.5.0~camlp4
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-algebra.8.5.0 coq.8.5.0~camlp4
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-algebra.8.5.0 coq.8.5.0~camlp4
Total: 4 M
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Complex_field.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fraction_field.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Complex_field.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/ZUP.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_of_group_hom.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fraction_field.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_quotient.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart2.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fmap.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ideal.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sets.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_module.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Zring.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_hom_factor.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_kernel.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_module.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart2.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fmap.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_quotient.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Hom_module.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_power.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Tiroirs.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Subcat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Qfield.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/ZUP.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sets.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts2.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_kernel.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_group.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cantor_Bernstein.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_group.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories2.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_util.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_util.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_util.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cartesian.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Complex_field.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_module.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Hom_module.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_util.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Union.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_sgroup.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_kernel.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts2.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Inter.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts3.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fraction_field.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_module.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_kernel.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sets.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_util.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_group.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ideal.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_hom_factor.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_group.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_of_group_hom.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fmap.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Fpart2.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_util.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_group.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cantor_Bernstein.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_util.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Z_group_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_util.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cartesian.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Subcat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_monoid.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Tiroirs.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_group.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_module.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_monoid.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts3.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Inter.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Union.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_quotient.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Endo_set.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_sgroup.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts2.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/ZUP.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Diff.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cantor_Bernstein.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Hom_module.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Operation_of_monoid.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_module.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_util.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Singleton.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories2.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_util.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ideal.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_facts.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_group.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Operation_of_monoid.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_group.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Zring.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Set_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_monoid.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Parts3.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_kernel.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Union.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_module.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_hom_factor.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cartesian.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_of_group_hom.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_cat.vo
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Tiroirs.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Zring.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_kernel.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_module.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Subcat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_monoid.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Ring_util.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_util.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_module.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_group.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Inter.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_abelian_monoid.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_group.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_power.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_group.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Free_monoid.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_kernel.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Generated_monoid.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Endo_set.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_sgroup.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Singleton.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_group.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Diff.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_facts.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Abelian_group_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Singleton.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sub_monoid.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Diff.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Module_kernel.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_kernel.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Categories2.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_power.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Operation_of_monoid.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Algebra.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Group_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Endo_set.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Monoid_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Sgroup_facts.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Field_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Integral_domain_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Set_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_cat.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Qfield.v
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Set_cat.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Qfield.glob
../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/Algebra/Cfield_cat.glob
opam remove -y coq-algebra.8.5.0