« Up

orb-stab dev Error with dependencies

(2020-02-20 10:20:10 UTC)

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
num                 1.3         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.09.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.0      Official release 4.09.0
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "dev@clarus.me"
homepage: "https://github.com/coq-contribs/orb-stab"
license: "GNU Lesser Public License"
build: [
  ["coq_makefile" "-f" "Make" "-o" "Makefile"]
  [make "-j%{jobs}%"]
  [make "install"]
]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/OrbStab"]
depends: [
  "ocaml"
  "coq" {= "dev"}
  "coq-algebra" {= "dev"}
  "coq-lin-alg" {= "dev"}
]
tags: [ "keyword:orbit" "keyword:stabilizer" "keyword:inclusion exclusion" "category:Mathematics/Algebra" "date:2008-01-5" ]
authors: [ "Robert Kam <rkam2001@hotmail.com>" ]
synopsis: "Finite orbit-stabilizer theorem."
description:
  "Finite orbit-stabilizer theorem, based on Rahbar Virk's lecture notes. A large portion of the work was a simplified version of the inclusion-exclusion principle. Requires Loic Pottier's Algebra contribution, and Jasper Stein's Linear Algebra contribution."
flags: light-uninstall
url {
  src: "git+https://github.com/coq-contribs/orb-stab.git#master"
}

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-orb-stab.dev coq.8.11.dev
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.11.dev).
The following dependencies couldn't be met:
  - coq-orb-stab -> coq-lin-alg >= dev
      no matching version
No solution found, exiting

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

Command
opam remove -y coq; opam install -y --show-action --unlock-base coq-orb-stab.dev
Return code
5120
Output
The following actions will be performed:
  - remove coq 8.11.dev
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[WARNING] While removing coq.8.11.dev: not removing files that changed since:
            - share/texmf/tex/latex/misc/coqdoc.sty
            - man/man1/coqwc.1
            - man/man1/coqtop.opt.1
            - man/man1/coqtop.byte.1
            - man/man1/coqtop.1
            - man/man1/coqide.1
            - man/man1/coqdoc.1
            - man/man1/coqdep.1
            - man/man1/coqchk.1
            - man/man1/coqc.1
            - man/man1/coq_makefile.1
            - man/man1/coq-tex.1
            - lib/coq/vernac/vernacstate.cmx
            - lib/coq/vernac/vernacstate.cmi
            - lib/coq/vernac/vernacprop.cmx
            - lib/coq/vernac/vernacprop.cmi
            - lib/coq/vernac/vernacinterp.cmx
            - lib/coq/vernac/vernacinterp.cmi
            - lib/coq/vernac/vernacextend.cmx
            - lib/coq/vernac/vernacextend.cmi
            - lib/coq/vernac/vernacexpr.cmx
            - lib/coq/vernac/vernacexpr.cmi
            - lib/coq/vernac/vernacentries.cmx
            - lib/coq/vernac/vernacentries.cmi
            - lib/coq/vernac/vernac.cmxa
            - lib/coq/vernac/vernac.cma
            - lib/coq/vernac/vernac.a
            - lib/coq/vernac/topfmt.cmx
            - lib/coq/vernac/topfmt.cmi
            - lib/coq/vernac/search.cmx
            - lib/coq/vernac/search.cmi
            - lib/coq/vernac/record.cmx
            - lib/coq/vernac/record.cmi
            - lib/coq/vernac/recLemmas.cmx
            - lib/coq/vernac/recLemmas.cmi
            - lib/coq/vernac/pvernac.cmx
            - lib/coq/vernac/pvernac.cmi
            - lib/coq/vernac/proof_using.cmx
            - lib/coq/vernac/proof_using.cmi
            - lib/coq/vernac/prettyp.cmx
            - lib/coq/vernac/prettyp.cmi
            - lib/coq/vernac/ppvernac.cmx
            - lib/coq/vernac/ppvernac.cmi
            - lib/coq/vernac/obligations.cmx
            - lib/coq/vernac/obligations.cmi
            - lib/coq/vernac/mltop.cmx
            - lib/coq/vernac/mltop.cmi
            - lib/coq/vernac/metasyntax.cmx
            - lib/coq/vernac/metasyntax.cmi
            - lib/coq/vernac/locality.cmx
            - lib/coq/vernac/locality.cmi
            - lib/coq/vernac/loadpath.cmx
            - lib/coq/vernac/loadpath.cmi
            - lib/coq/vernac/library.cmx
            - lib/coq/vernac/library.cmi
            - lib/coq/vernac/lemmas.cmx
            - lib/coq/vernac/lemmas.cmi
            - lib/coq/vernac/indschemes.cmx
            - lib/coq/vernac/indschemes.cmi
            - lib/coq/vernac/himsg.cmx
            - lib/coq/vernac/himsg.cmi
            - lib/coq/vernac/g_vernac.cmx
            - lib/coq/vernac/g_vernac.cmi
            - lib/coq/vernac/g_proofs.cmx
            - lib/coq/vernac/g_proofs.cmi
            - lib/coq/vernac/egramml.cmx
            - lib/coq/vernac/egramml.cmi
            - lib/coq/vernac/egramcoq.cmx
            - lib/coq/vernac/egramcoq.cmi
            - lib/coq/vernac/declaremods.cmx
            - lib/coq/vernac/declaremods.cmi
            - lib/coq/vernac/declareUniv.cmx
            - lib/coq/vernac/declareUniv.cmi
            - lib/coq/vernac/declareObl.cmx
            - lib/coq/vernac/declareObl.cmi
            - lib/coq/vernac/declareInd.cmx
            - lib/coq/vernac/declareInd.cmi
            - lib/coq/vernac/declareDef.cmx
            - lib/coq/vernac/declareDef.cmi
            - lib/coq/vernac/comProgramFixpoint.cmx
            - lib/coq/vernac/comProgramFixpoint.cmi
            - lib/coq/vernac/comPrimitive.cmx
            - lib/coq/vernac/comPrimitive.cmi
            - lib/coq/vernac/comInductive.cmx
            - lib/coq/vernac/comInductive.cmi
            - lib/coq/vernac/comFixpoint.cmx
            - lib/coq/vernac/comFixpoint.cmi
            - lib/coq/vernac/comDefinition.cmx
            - lib/coq/vernac/comDefinition.cmi
            - lib/coq/vernac/comAssumption.cmx
            - lib/coq/vernac/comAssumption.cmi
            - lib/coq/vernac/comArguments.cmx
            - lib/coq/vernac/comArguments.cmi
            - lib/coq/vernac/classes.cmx
            - lib/coq/vernac/classes.cmi
            - lib/coq/vernac/class.cmx
            - lib/coq/vernac/class.cmi
            - lib/coq/vernac/canonical.cmx
            - lib/coq/vernac/canonical.cmi
            - lib/coq/vernac/auto_ind_decl.cmx
            - lib/coq/vernac/auto_ind_decl.cmi
            - lib/coq/vernac/attributes.cmx
            - lib/coq/vernac/attributes.cmi
            - lib/coq/vernac/assumptions.cmx
            - lib/coq/vernac/assumptions.cmi
            - lib/coq/user-contrib/Ltac2/tac2types.cmi
            - lib/coq/user-contrib/Ltac2/tac2tactics.cmx
            - lib/coq/user-contrib/Ltac2/tac2tactics.cmi
            - lib/coq/user-contrib/Ltac2/tac2stdlib.cmx
            - lib/coq/user-contrib/Ltac2/tac2stdlib.cmi
            - lib/coq/user-contrib/Ltac2/tac2quote.cmx
            - lib/coq/user-contrib/Ltac2/tac2quote.cmi
            - lib/coq/user-contrib/Ltac2/tac2qexpr.cmi
            - lib/coq/user-contrib/Ltac2/tac2print.cmx
            - lib/coq/user-contrib/Ltac2/tac2print.cmi
            - lib/coq/user-contrib/Ltac2/tac2match.cmx
            - lib/coq/user-contrib/Ltac2/tac2match.cmi
            - lib/coq/user-contrib/Ltac2/tac2interp.cmx
            - lib/coq/user-contrib/Ltac2/tac2interp.cmi
            - lib/coq/user-contrib/Ltac2/tac2intern.cmx
            - lib/coq/user-contrib/Ltac2/tac2intern.cmi
            - lib/coq/user-contrib/Ltac2/tac2ffi.cmx
            - lib/coq/user-contrib/Ltac2/tac2ffi.cmi
            - lib/coq/user-contrib/Ltac2/tac2extffi.cmx
            - lib/coq/user-contrib/Ltac2/tac2extffi.cmi
            - lib/coq/user-contrib/Ltac2/tac2expr.cmi
            - lib/coq/user-contrib/Ltac2/tac2env.cmx
            - lib/coq/user-contrib/Ltac2/tac2env.cmi
            - lib/coq/user-contrib/Ltac2/tac2entries.cmx
            - lib/coq/user-contrib/Ltac2/tac2entries.cmi
            - lib/coq/user-contrib/Ltac2/tac2dyn.cmx
            - lib/coq/user-contrib/Ltac2/tac2dyn.cmi
            - lib/coq/user-contrib/Ltac2/tac2core.cmx
            - lib/coq/user-contrib/Ltac2/tac2core.cmi
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.o
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmxs
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmx
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmo
            - lib/coq/user-contrib/Ltac2/ltac2_plugin.cmi
            - lib/coq/user-contrib/Ltac2/g_ltac2.cmx
            - lib/coq/user-contrib/Ltac2/String.vos
            - lib/coq/user-contrib/Ltac2/String.vo
            - lib/coq/user-contrib/Ltac2/String.v
            - lib/coq/user-contrib/Ltac2/String.glob
            - lib/coq/user-contrib/Ltac2/Std.vos
            - lib/coq/user-contrib/Ltac2/Std.vo
            - lib/coq/user-contrib/Ltac2/Std.v
            - lib/coq/user-contrib/Ltac2/Std.glob
            - lib/coq/user-contrib/Ltac2/Pattern.vos
            - lib/coq/user-contrib/Ltac2/Pattern.vo
            - lib/coq/user-contrib/Ltac2/Pattern.v
            - lib/coq/user-contrib/Ltac2/Pattern.glob
            - lib/coq/user-contrib/Ltac2/Option.vos
            - lib/coq/user-contrib/Ltac2/Option.vo
            - lib/coq/user-contrib/Ltac2/Option.v
            - lib/coq/user-contrib/Ltac2/Option.glob
            - lib/coq/user-contrib/Ltac2/Notations.vos
            - lib/coq/user-contrib/Ltac2/Notations.vo
            - lib/coq/user-contrib/Ltac2/Notations.v
            - lib/coq/user-contrib/Ltac2/Notations.glob
            - lib/coq/user-contrib/Ltac2/Message.vos
            - lib/coq/user-contrib/Ltac2/Message.vo
            - lib/coq/user-contrib/Ltac2/Message.v
            - lib/coq/user-contrib/Ltac2/Message.glob
            - lib/coq/user-contrib/Ltac2/Ltac2.vos
            - lib/coq/user-contrib/Ltac2/Ltac2.vo
            - lib/coq/user-contrib/Ltac2/Ltac2.v
            - lib/coq/user-contrib/Ltac2/Ltac2.glob
            - lib/coq/user-contrib/Ltac2/Ltac1.vos
            - lib/coq/user-contrib/Ltac2/Ltac1.vo
            - lib/coq/user-contrib/Ltac2/Ltac1.v
            - lib/coq/user-contrib/Ltac2/Ltac1.glob
            - lib/coq/user-contrib/Ltac2/List.vos
            - lib/coq/user-contrib/Ltac2/List.vo
            - lib/coq/user-contrib/Ltac2/List.v
            - lib/coq/user-contrib/Ltac2/List.glob
            - lib/coq/user-contrib/Ltac2/Int.vos
            - lib/coq/user-contrib/Ltac2/Int.vo
            - lib/coq/user-contrib/Ltac2/Int.v
            - lib/coq/user-contrib/Ltac2/Int.glob
            - lib/coq/user-contrib/Ltac2/Init.vos
            - lib/coq/user-contrib/Ltac2/Init.vo
            - lib/coq/user-contrib/Ltac2/Init.v
            - lib/coq/user-contrib/Ltac2/Init.glob
            - lib/coq/user-contrib/Ltac2/Ident.vos
            - lib/coq/user-contrib/Ltac2/Ident.vo
            - lib/coq/user-contrib/Ltac2/Ident.v
            - lib/coq/user-contrib/Ltac2/Ident.glob
            - lib/coq/user-contrib/Ltac2/Fresh.vos
            - lib/coq/user-contrib/Ltac2/Fresh.vo
            - lib/coq/user-contrib/Ltac2/Fresh.v
            - lib/coq/user-contrib/Ltac2/Fresh.glob
            - lib/coq/user-contrib/Ltac2/Env.vos
            - lib/coq/user-contrib/Ltac2/Env.vo
            - lib/coq/user-contrib/Ltac2/Env.v
            - lib/coq/user-contrib/Ltac2/Env.glob
            - lib/coq/user-contrib/Ltac2/Control.vos
            - lib/coq/user-contrib/Ltac2/Control.vo
            - lib/coq/user-contrib/Ltac2/Control.v
            - lib/coq/user-contrib/Ltac2/Control.glob
            - lib/coq/user-contrib/Ltac2/Constr.vos
            - lib/coq/user-contrib/Ltac2/Constr.vo
            - lib/coq/user-contrib/Ltac2/Constr.v
            - lib/coq/user-contrib/Ltac2/Constr.glob
            - lib/coq/user-contrib/Ltac2/Char.vos
            - lib/coq/user-contrib/Ltac2/Char.vo
            - lib/coq/user-contrib/Ltac2/Char.v
            - lib/coq/user-contrib/Ltac2/Char.glob
            - lib/coq/user-contrib/Ltac2/Bool.vos
            - lib/coq/user-contrib/Ltac2/Bool.vo
            - lib/coq/user-contrib/Ltac2/Bool.v
            - lib/coq/user-contrib/Ltac2/Bool.glob
            - lib/coq/user-contrib/Ltac2/Array.vos
            - lib/coq/user-contrib/Ltac2/Array.vo
            - lib/coq/user-contrib/Ltac2/Array.v
            - lib/coq/user-contrib/Ltac2/Array.glob
            - lib/coq/toplevel/workerLoop.cmx
            - lib/coq/toplevel/workerLoop.cmi
            - lib/coq/toplevel/vernac.cmx
            - lib/coq/toplevel/vernac.cmi
            - lib/coq/toplevel/usage.cmx
            - lib/coq/toplevel/usage.cmi
            - lib/coq/toplevel/toplevel.cmxa
            - lib/coq/toplevel/toplevel.cma
            - lib/coq/toplevel/toplevel.a
            - lib/coq/toplevel/g_toplevel.cmx
            - lib/coq/toplevel/g_toplevel.cmi
            - lib/coq/toplevel/coqtop.cmx
            - lib/coq/toplevel/coqtop.cmi
            - lib/coq/toplevel/coqloop.cmx
            - lib/coq/toplevel/coqloop.cmi
            - lib/coq/toplevel/coqinit.cmx
            - lib/coq/toplevel/coqinit.cmi
            - lib/coq/toplevel/coqcargs.cmx
            - lib/coq/toplevel/coqcargs.cmi
            - lib/coq/toplevel/coqc.cmx
            - lib/coq/toplevel/coqc.cmi
            - lib/coq/toplevel/coqargs.cmx
            - lib/coq/toplevel/coqargs.cmi
            - lib/coq/toplevel/ccompile.cmx
            - lib/coq/toplevel/ccompile.cmi
            - lib/coq/topbin/coqtop_bin.cmx
            - lib/coq/topbin/coqtacticworker_bin.cmx
            - lib/coq/topbin/coqqueryworker_bin.cmx
            - lib/coq/topbin/coqproofworker_bin.cmx
            - lib/coq/topbin/coqc_bin.cmx
            - lib/coq/tools/make-one-time-file.py
            - lib/coq/tools/make-both-time-files.py
            - lib/coq/tools/make-both-single-timing-files.py
            - lib/coq/tools/coqdoc/coqdoc.sty
            - lib/coq/tools/coqdoc/coqdoc.css
            - lib/coq/tools/TimeFileMaker.py
            - lib/coq/tools/CoqMakefile.in
            - lib/coq/theories/ZArith/auxiliary.vos
            - lib/coq/theories/ZArith/auxiliary.vo
            - lib/coq/theories/ZArith/auxiliary.v
            - lib/coq/theories/ZArith/auxiliary.glob
            - lib/coq/theories/ZArith/Zwf.vos
            - lib/coq/theories/ZArith/Zwf.vo
            - lib/coq/theories/ZArith/Zwf.v
            - lib/coq/theories/ZArith/Zwf.glob
            - lib/coq/theories/ZArith/Zquot.vos
            - lib/coq/theories/ZArith/Zquot.vo
            - lib/coq/theories/ZArith/Zquot.v
            - lib/coq/theories/ZArith/Zquot.glob
            - lib/coq/theories/ZArith/Zpower.vos
            - lib/coq/theories/ZArith/Zpower.vo
            - lib/coq/theories/ZArith/Zpower.v
            - lib/coq/theories/ZArith/Zpower.glob
            - lib/coq/theories/ZArith/Zpow_facts.vos
            - lib/coq/theories/ZArith/Zpow_facts.vo
            - lib/coq/theories/ZArith/Zpow_facts.v
            - lib/coq/theories/ZArith/Zpow_facts.glob
            - lib/coq/theories/ZArith/Zpow_def.vos
            - lib/coq/theories/ZArith/Zpow_def.vo
            - lib/coq/theories/ZArith/Zpow_def.v
            - lib/coq/theories/ZArith/Zpow_def.glob
            - lib/coq/theories/ZArith/Zpow_alt.vos
            - lib/coq/theories/ZArith/Zpow_alt.vo
            - lib/coq/theories/ZArith/Zpow_alt.v
            - lib/coq/theories/ZArith/Zpow_alt.glob
            - lib/coq/theories/ZArith/Zorder.vos
            - lib/coq/theories/ZArith/Zorder.vo
            - lib/coq/theories/ZArith/Zorder.v
            - lib/coq/theories/ZArith/Zorder.glob
            - lib/coq/theories/ZArith/Znumtheory.vos
            - lib/coq/theories/ZArith/Znumtheory.vo
            - lib/coq/theories/ZArith/Znumtheory.v
            - lib/coq/theories/ZArith/Znumtheory.glob
            - lib/coq/theories/ZArith/Znat.vos
            - lib/coq/theories/ZArith/Znat.vo
            - lib/coq/theories/ZArith/Znat.v
            - lib/coq/theories/ZArith/Znat.glob
            - lib/coq/theories/ZArith/Zmisc.vos
            - lib/coq/theories/ZArith/Zmisc.vo
            - lib/coq/theories/ZArith/Zmisc.v
            - lib/coq/theories/ZArith/Zmisc.glob
            - lib/coq/theories/ZArith/Zminmax.vos
            - lib/coq/theories/ZArith/Zminmax.vo
            - lib/coq/theories/ZArith/Zminmax.v
            - lib/coq/theories/ZArith/Zminmax.glob
            - lib/coq/theories/ZArith/Zmin.vos
            - lib/coq/theories/ZArith/Zmin.vo
            - lib/coq/theories/ZArith/Zmin.v
            - lib/coq/theories/ZArith/Zmin.glob
            - lib/coq/theories/ZArith/Zmax.vos
            - lib/coq/theories/ZArith/Zmax.vo
            - lib/coq/theories/ZArith/Zmax.v
            - lib/coq/theories/ZArith/Zmax.glob
            - lib/coq/theories/ZArith/Zhints.vos
            - lib/coq/theories/ZArith/Zhints.vo
            - lib/coq/theories/ZArith/Zhints.v
            - lib/coq/theories/ZArith/Zhints.glob
            - lib/coq/theories/ZArith/Zgcd_alt.vos
            - lib/coq/theories/ZArith/Zgcd_alt.vo
            - lib/coq/theories/ZArith/Zgcd_alt.v
            - lib/coq/theories/ZArith/Zgcd_alt.glob
            - lib/coq/theories/ZArith/Zeven.vos
            - lib/coq/theories/ZArith/Zeven.vo
            - lib/coq/theories/ZArith/Zeven.v
            - lib/coq/theories/ZArith/Zeven.glob
            - lib/coq/theories/ZArith/Zeuclid.vos
            - lib/coq/theories/ZArith/Zeuclid.vo
            - lib/coq/theories/ZArith/Zeuclid.v
            - lib/coq/theories/ZArith/Zeuclid.glob
            - lib/coq/theories/ZArith/Zdiv.vos
            - lib/coq/theories/ZArith/Zdiv.vo
            - lib/coq/theories/ZArith/Zdiv.v
            - lib/coq/theories/ZArith/Zdiv.glob
            - lib/coq/theories/ZArith/Zdigits.vos
            - lib/coq/theories/ZArith/Zdigits.vo
            - lib/coq/theories/ZArith/Zdigits.v
            - lib/coq/theories/ZArith/Zdigits.glob
            - lib/coq/theories/ZArith/Zcomplements.vos
            - lib/coq/theories/ZArith/Zcomplements.vo
            - lib/coq/theories/ZArith/Zcomplements.v
            - lib/coq/theories/ZArith/Zcomplements.glob
            - lib/coq/theories/ZArith/Zcompare.vos
            - lib/coq/theories/ZArith/Zcompare.vo
            - lib/coq/theories/ZArith/Zcompare.v
            - lib/coq/theories/ZArith/Zcompare.glob
            - lib/coq/theories/ZArith/Zbool.vos
            - lib/coq/theories/ZArith/Zbool.vo
            - lib/coq/theories/ZArith/Zbool.v
            - lib/coq/theories/ZArith/Zbool.glob
            - lib/coq/theories/ZArith/Zabs.vos
            - lib/coq/theories/ZArith/Zabs.vo
            - lib/coq/theories/ZArith/Zabs.v
            - lib/coq/theories/ZArith/Zabs.glob
            - lib/coq/theories/ZArith/ZArith_dec.vos
            - lib/coq/theories/ZArith/ZArith_dec.vo
            - lib/coq/theories/ZArith/ZArith_dec.v
            - lib/coq/theories/ZArith/ZArith_dec.glob
            - lib/coq/theories/ZArith/ZArith_base.vos
            - lib/coq/theories/ZArith/ZArith_base.vo
            - lib/coq/theories/ZArith/ZArith_base.v
            - lib/coq/theories/ZArith/ZArith_base.glob
            - lib/coq/theories/ZArith/ZArith.vos
            - lib/coq/theories/ZArith/ZArith.vo
            - lib/coq/theories/ZArith/ZArith.v
            - lib/coq/theories/ZArith/ZArith.glob
            - lib/coq/theories/ZArith/Wf_Z.vos
            - lib/coq/theories/ZArith/Wf_Z.vo
            - lib/coq/theories/ZArith/Wf_Z.v
            - lib/coq/theories/ZArith/Wf_Z.glob
            - lib/coq/theories/ZArith/Int.vos
            - lib/coq/theories/ZArith/Int.vo
            - lib/coq/theories/ZArith/Int.v
            - lib/coq/theories/ZArith/Int.glob
            - lib/coq/theories/ZArith/BinIntDef.vos
            - lib/coq/theories/ZArith/BinIntDef.vo
            - lib/coq/theories/ZArith/BinIntDef.v
            - lib/coq/theories/ZArith/BinIntDef.glob
            - lib/coq/theories/ZArith/BinInt.vos
            - lib/coq/theories/ZArith/BinInt.vo
            - lib/coq/theories/ZArith/BinInt.v
            - lib/coq/theories/ZArith/BinInt.glob
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_auxiliary.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zwf.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zquot.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpower.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_facts.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_def.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zpow_alt.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zorder.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znumtheory.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znumtheory.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znumtheory.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znumtheory.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znat.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znat.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znat.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Znat.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmisc.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmisc.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmisc.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmisc.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zminmax.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmin.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zmax.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zhints.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zgcd_alt.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeven.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeuclid.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeuclid.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeuclid.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zeuclid.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdiv.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdiv.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdiv.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdiv.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdigits.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdigits.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdigits.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zdigits.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcomplements.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcomplements.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcomplements.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcomplements.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcompare.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcompare.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcompare.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zcompare.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zbool.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zbool.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zbool.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zbool.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zabs.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zabs.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zabs.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Zabs.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_dec.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_dec.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_dec.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_dec.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_base.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_base.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_base.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith_base.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_ZArith.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Wf_Z.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Wf_Z.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Wf_Z.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Wf_Z.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Int.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Int.cmxs
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Int.cmx
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_Int.cmi
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_BinIntDef.o
            - lib/coq/theories/ZArith/.coq-native/NCoq_ZArith_BinIntDef.cmxs
[...] truncated
            - lib/coq/plugins/btauto/Btauto.v
            - lib/coq/plugins/btauto/Btauto.glob
            - lib/coq/plugins/btauto/Algebra.vos
            - lib/coq/plugins/btauto/Algebra.vo
            - lib/coq/plugins/btauto/Algebra.v
            - lib/coq/plugins/btauto/Algebra.glob
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.o
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmxs
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmx
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Reflect.cmi
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.o
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmxs
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmx
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Btauto.cmi
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.o
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmxs
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmx
            - lib/coq/plugins/btauto/.coq-native/NCoq_btauto_Algebra.cmi
            - lib/coq/parsing/tok.cmx
            - lib/coq/parsing/tok.cmi
            - lib/coq/parsing/ppextend.cmx
            - lib/coq/parsing/ppextend.cmi
            - lib/coq/parsing/pcoq.cmx
            - lib/coq/parsing/pcoq.cmi
            - lib/coq/parsing/parsing.cmxa
            - lib/coq/parsing/parsing.cma
            - lib/coq/parsing/parsing.a
            - lib/coq/parsing/notgram_ops.cmx
            - lib/coq/parsing/notgram_ops.cmi
            - lib/coq/parsing/notation_gram.cmx
            - lib/coq/parsing/notation_gram.cmi
            - lib/coq/parsing/g_prim.cmx
            - lib/coq/parsing/g_prim.cmi
            - lib/coq/parsing/g_constr.cmx
            - lib/coq/parsing/g_constr.cmi
            - lib/coq/parsing/extend.cmx
            - lib/coq/parsing/extend.cmi
            - lib/coq/parsing/cLexer.cmx
            - lib/coq/parsing/cLexer.cmi
            - lib/coq/library/summary.cmx
            - lib/coq/library/summary.cmi
            - lib/coq/library/states.cmx
            - lib/coq/library/states.cmi
            - lib/coq/library/nametab.cmx
            - lib/coq/library/nametab.cmi
            - lib/coq/library/library.cmxa
            - lib/coq/library/library.cma
            - lib/coq/library/library.a
            - lib/coq/library/libobject.cmx
            - lib/coq/library/libobject.cmi
            - lib/coq/library/libnames.cmx
            - lib/coq/library/libnames.cmi
            - lib/coq/library/lib.cmx
            - lib/coq/library/lib.cmi
            - lib/coq/library/goptions.cmx
            - lib/coq/library/goptions.cmi
            - lib/coq/library/globnames.cmx
            - lib/coq/library/globnames.cmi
            - lib/coq/library/global.cmx
            - lib/coq/library/global.cmi
            - lib/coq/library/coqlib.cmx
            - lib/coq/library/coqlib.cmi
            - lib/coq/lib/xml_datatype.cmi
            - lib/coq/lib/util.cmx
            - lib/coq/lib/util.cmi
            - lib/coq/lib/system.cmx
            - lib/coq/lib/system.cmi
            - lib/coq/lib/stateid.cmx
            - lib/coq/lib/stateid.cmi
            - lib/coq/lib/spawn.cmx
            - lib/coq/lib/spawn.cmi
            - lib/coq/lib/rtree.cmx
            - lib/coq/lib/rtree.cmi
            - lib/coq/lib/remoteCounter.cmx
            - lib/coq/lib/remoteCounter.cmi
            - lib/coq/lib/pp_diff.cmx
            - lib/coq/lib/pp_diff.cmi
            - lib/coq/lib/pp.cmx
            - lib/coq/lib/pp.cmi
            - lib/coq/lib/loc.cmx
            - lib/coq/lib/loc.cmi
            - lib/coq/lib/lib.cmxa
            - lib/coq/lib/lib.cma
            - lib/coq/lib/lib.a
            - lib/coq/lib/hook.cmx
            - lib/coq/lib/hook.cmi
            - lib/coq/lib/genarg.cmx
            - lib/coq/lib/genarg.cmi
            - lib/coq/lib/future.cmx
            - lib/coq/lib/future.cmi
            - lib/coq/lib/flags.cmx
            - lib/coq/lib/flags.cmi
            - lib/coq/lib/feedback.cmx
            - lib/coq/lib/feedback.cmi
            - lib/coq/lib/explore.cmx
            - lib/coq/lib/explore.cmi
            - lib/coq/lib/envars.cmx
            - lib/coq/lib/envars.cmi
            - lib/coq/lib/dAst.cmx
            - lib/coq/lib/dAst.cmi
            - lib/coq/lib/coqProject_file.cmx
            - lib/coq/lib/coqProject_file.cmi
            - lib/coq/lib/control.cmx
            - lib/coq/lib/control.cmi
            - lib/coq/lib/cWarnings.cmx
            - lib/coq/lib/cWarnings.cmi
            - lib/coq/lib/cProfile.cmx
            - lib/coq/lib/cProfile.cmi
            - lib/coq/lib/cErrors.cmx
            - lib/coq/lib/cErrors.cmi
            - lib/coq/lib/cAst.cmx
            - lib/coq/lib/cAst.cmi
            - lib/coq/lib/aux_file.cmx
            - lib/coq/lib/aux_file.cmi
            - lib/coq/lib/acyclicGraph.cmx
            - lib/coq/lib/acyclicGraph.cmi
            - lib/coq/kernel/vmvalues.cmx
            - lib/coq/kernel/vmvalues.cmi
            - lib/coq/kernel/vm.cmx
            - lib/coq/kernel/vm.cmi
            - lib/coq/kernel/vconv.cmx
            - lib/coq/kernel/vconv.cmi
            - lib/coq/kernel/vars.cmx
            - lib/coq/kernel/vars.cmi
            - lib/coq/kernel/univ.cmx
            - lib/coq/kernel/univ.cmi
            - lib/coq/kernel/uint63.cmx
            - lib/coq/kernel/uint63.cmi
            - lib/coq/kernel/uGraph.cmx
            - lib/coq/kernel/uGraph.cmi
            - lib/coq/kernel/typeops.cmx
            - lib/coq/kernel/typeops.cmi
            - lib/coq/kernel/type_errors.cmx
            - lib/coq/kernel/type_errors.cmi
            - lib/coq/kernel/transparentState.cmx
            - lib/coq/kernel/transparentState.cmi
            - lib/coq/kernel/term_typing.cmx
            - lib/coq/kernel/term_typing.cmi
            - lib/coq/kernel/term.cmx
            - lib/coq/kernel/term.cmi
            - lib/coq/kernel/subtyping.cmx
            - lib/coq/kernel/subtyping.cmi
            - lib/coq/kernel/sorts.cmx
            - lib/coq/kernel/sorts.cmi
            - lib/coq/kernel/section.cmx
            - lib/coq/kernel/section.cmi
            - lib/coq/kernel/safe_typing.cmx
            - lib/coq/kernel/safe_typing.cmi
            - lib/coq/kernel/retypeops.cmx
            - lib/coq/kernel/retypeops.cmi
            - lib/coq/kernel/retroknowledge.cmx
            - lib/coq/kernel/retroknowledge.cmi
            - lib/coq/kernel/reduction.cmx
            - lib/coq/kernel/reduction.cmi
            - lib/coq/kernel/primred.cmx
            - lib/coq/kernel/primred.cmi
            - lib/coq/kernel/opaqueproof.cmx
            - lib/coq/kernel/opaqueproof.cmi
            - lib/coq/kernel/nativevalues.cmx
            - lib/coq/kernel/nativevalues.cmi
            - lib/coq/kernel/nativelibrary.cmx
            - lib/coq/kernel/nativelibrary.cmi
            - lib/coq/kernel/nativelib.cmx
            - lib/coq/kernel/nativelib.cmi
            - lib/coq/kernel/nativelambda.cmx
            - lib/coq/kernel/nativelambda.cmi
            - lib/coq/kernel/nativeconv.cmx
            - lib/coq/kernel/nativeconv.cmi
            - lib/coq/kernel/nativecode.cmx
            - lib/coq/kernel/nativecode.cmi
            - lib/coq/kernel/names.cmx
            - lib/coq/kernel/names.cmi
            - lib/coq/kernel/modops.cmx
            - lib/coq/kernel/modops.cmi
            - lib/coq/kernel/mod_typing.cmx
            - lib/coq/kernel/mod_typing.cmi
            - lib/coq/kernel/mod_subst.cmx
            - lib/coq/kernel/mod_subst.cmi
            - lib/coq/kernel/kernel.cmxa
            - lib/coq/kernel/kernel.cma
            - lib/coq/kernel/kernel.a
            - lib/coq/kernel/inferCumulativity.cmx
            - lib/coq/kernel/inferCumulativity.cmi
            - lib/coq/kernel/inductive.cmx
            - lib/coq/kernel/inductive.cmi
            - lib/coq/kernel/indtypes.cmx
            - lib/coq/kernel/indtypes.cmi
            - lib/coq/kernel/indTyping.cmx
            - lib/coq/kernel/indTyping.cmi
            - lib/coq/kernel/float64.cmx
            - lib/coq/kernel/float64.cmi
            - lib/coq/kernel/evar.cmx
            - lib/coq/kernel/evar.cmi
            - lib/coq/kernel/esubst.cmx
            - lib/coq/kernel/esubst.cmi
            - lib/coq/kernel/environ.cmx
            - lib/coq/kernel/environ.cmi
            - lib/coq/kernel/entries.cmx
            - lib/coq/kernel/entries.cmi
            - lib/coq/kernel/declareops.cmx
            - lib/coq/kernel/declareops.cmi
            - lib/coq/kernel/declarations.cmx
            - lib/coq/kernel/declarations.cmi
            - lib/coq/kernel/csymtable.cmx
            - lib/coq/kernel/csymtable.cmi
            - lib/coq/kernel/copcodes.cmx
            - lib/coq/kernel/copcodes.cmi
            - lib/coq/kernel/cooking.cmx
            - lib/coq/kernel/cooking.cmi
            - lib/coq/kernel/conv_oracle.cmx
            - lib/coq/kernel/conv_oracle.cmi
            - lib/coq/kernel/context.cmx
            - lib/coq/kernel/context.cmi
            - lib/coq/kernel/constr.cmx
            - lib/coq/kernel/constr.cmi
            - lib/coq/kernel/clambda.cmx
            - lib/coq/kernel/clambda.cmi
            - lib/coq/kernel/cemitcodes.cmx
            - lib/coq/kernel/cemitcodes.cmi
            - lib/coq/kernel/cbytegen.cmx
            - lib/coq/kernel/cbytegen.cmi
            - lib/coq/kernel/cbytecodes.cmx
            - lib/coq/kernel/cbytecodes.cmi
            - lib/coq/kernel/cPrimitives.cmx
            - lib/coq/kernel/cPrimitives.cmi
            - lib/coq/kernel/cClosure.cmx
            - lib/coq/kernel/cClosure.cmi
            - lib/coq/kernel/byterun/libcoqrun.a
            - lib/coq/kernel/byterun/dllcoqrun.so
            - lib/coq/interp/syntax_def.cmx
            - lib/coq/interp/syntax_def.cmi
            - lib/coq/interp/stdarg.cmx
            - lib/coq/interp/stdarg.cmi
            - lib/coq/interp/smartlocate.cmx
            - lib/coq/interp/smartlocate.cmi
            - lib/coq/interp/reserve.cmx
            - lib/coq/interp/reserve.cmi
            - lib/coq/interp/numTok.cmx
            - lib/coq/interp/numTok.cmi
            - lib/coq/interp/notation_term.cmx
            - lib/coq/interp/notation_term.cmi
            - lib/coq/interp/notation_ops.cmx
            - lib/coq/interp/notation_ops.cmi
            - lib/coq/interp/notation.cmx
            - lib/coq/interp/notation.cmi
            - lib/coq/interp/modintern.cmx
            - lib/coq/interp/modintern.cmi
            - lib/coq/interp/interp.cmxa
            - lib/coq/interp/interp.cma
            - lib/coq/interp/interp.a
            - lib/coq/interp/implicit_quantifiers.cmx
            - lib/coq/interp/implicit_quantifiers.cmi
            - lib/coq/interp/impargs.cmx
            - lib/coq/interp/impargs.cmi
            - lib/coq/interp/genintern.cmx
            - lib/coq/interp/genintern.cmi
            - lib/coq/interp/dumpglob.cmx
            - lib/coq/interp/dumpglob.cmi
            - lib/coq/interp/deprecation.cmx
            - lib/coq/interp/deprecation.cmi
            - lib/coq/interp/decls.cmx
            - lib/coq/interp/decls.cmi
            - lib/coq/interp/constrintern.cmx
            - lib/coq/interp/constrintern.cmi
            - lib/coq/interp/constrextern.cmx
            - lib/coq/interp/constrextern.cmi
            - lib/coq/interp/constrexpr_ops.cmx
            - lib/coq/interp/constrexpr_ops.cmi
            - lib/coq/interp/constrexpr.cmx
            - lib/coq/interp/constrexpr.cmi
            - lib/coq/gramlib/.pack/gramlib__Ploc.cmx
            - lib/coq/gramlib/.pack/gramlib__Ploc.cmi
            - lib/coq/gramlib/.pack/gramlib__Plexing.cmx
            - lib/coq/gramlib/.pack/gramlib__Plexing.cmi
            - lib/coq/gramlib/.pack/gramlib__Grammar.cmx
            - lib/coq/gramlib/.pack/gramlib__Grammar.cmi
            - lib/coq/gramlib/.pack/gramlib__Gramext.cmx
            - lib/coq/gramlib/.pack/gramlib__Gramext.cmi
            - lib/coq/gramlib/.pack/gramlib.cmxa
            - lib/coq/gramlib/.pack/gramlib.cmx
            - lib/coq/gramlib/.pack/gramlib.cmi
            - lib/coq/gramlib/.pack/gramlib.cma
            - lib/coq/gramlib/.pack/gramlib.a
            - lib/coq/engine/univops.cmx
            - lib/coq/engine/univops.cmi
            - lib/coq/engine/univSubst.cmx
            - lib/coq/engine/univSubst.cmi
            - lib/coq/engine/univProblem.cmx
            - lib/coq/engine/univProblem.cmi
            - lib/coq/engine/univNames.cmx
            - lib/coq/engine/univNames.cmi
            - lib/coq/engine/univMinim.cmx
            - lib/coq/engine/univMinim.cmi
            - lib/coq/engine/univGen.cmx
            - lib/coq/engine/univGen.cmi
            - lib/coq/engine/uState.cmx
            - lib/coq/engine/uState.cmi
            - lib/coq/engine/termops.cmx
            - lib/coq/engine/termops.cmi
            - lib/coq/engine/proofview_monad.cmx
            - lib/coq/engine/proofview_monad.cmi
            - lib/coq/engine/proofview.cmx
            - lib/coq/engine/proofview.cmi
            - lib/coq/engine/nameops.cmx
            - lib/coq/engine/nameops.cmi
            - lib/coq/engine/namegen.cmx
            - lib/coq/engine/namegen.cmi
            - lib/coq/engine/logic_monad.cmx
            - lib/coq/engine/logic_monad.cmi
            - lib/coq/engine/ftactic.cmx
            - lib/coq/engine/ftactic.cmi
            - lib/coq/engine/evd.cmx
            - lib/coq/engine/evd.cmi
            - lib/coq/engine/evarutil.cmx
            - lib/coq/engine/evarutil.cmi
            - lib/coq/engine/evar_kinds.cmx
            - lib/coq/engine/evar_kinds.cmi
            - lib/coq/engine/engine.cmxa
            - lib/coq/engine/engine.cma
            - lib/coq/engine/engine.a
            - lib/coq/engine/eConstr.cmx
            - lib/coq/engine/eConstr.cmi
            - lib/coq/dllcoqrun.so
            - lib/coq/dev/top_printers.cmi
            - lib/coq/coqpp/coqpp_parser.cmi
            - lib/coq/coqpp/coqpp_parse.cmi
            - lib/coq/coqpp/coqpp_ast.cmi
            - lib/coq/config/coq_config.cmx
            - lib/coq/config/coq_config.cmi
            - lib/coq/config/config.cmxa
            - lib/coq/config/config.cma
            - lib/coq/config/config.a
            - lib/coq/clib/unionfind.cmx
            - lib/coq/clib/unionfind.cmi
            - lib/coq/clib/unicodetable.cmx
            - lib/coq/clib/unicodetable.cmi
            - lib/coq/clib/unicode.cmx
            - lib/coq/clib/unicode.cmi
            - lib/coq/clib/trie.cmx
            - lib/coq/clib/trie.cmi
            - lib/coq/clib/terminal.cmx
            - lib/coq/clib/terminal.cmi
            - lib/coq/clib/store.cmx
            - lib/coq/clib/store.cmi
            - lib/coq/clib/segmenttree.cmx
            - lib/coq/clib/segmenttree.cmi
            - lib/coq/clib/range.cmx
            - lib/coq/clib/range.cmi
            - lib/coq/clib/predicate.cmx
            - lib/coq/clib/predicate.cmi
            - lib/coq/clib/orderedType.cmx
            - lib/coq/clib/orderedType.cmi
            - lib/coq/clib/option.cmx
            - lib/coq/clib/option.cmi
            - lib/coq/clib/monad.cmx
            - lib/coq/clib/monad.cmi
            - lib/coq/clib/minisys.cmx
            - lib/coq/clib/minisys.cmi
            - lib/coq/clib/int.cmx
            - lib/coq/clib/int.cmi
            - lib/coq/clib/iStream.cmx
            - lib/coq/clib/iStream.cmi
            - lib/coq/clib/heap.cmx
            - lib/coq/clib/heap.cmi
            - lib/coq/clib/hashset.cmx
            - lib/coq/clib/hashset.cmi
            - lib/coq/clib/hashcons.cmx
            - lib/coq/clib/hashcons.cmi
            - lib/coq/clib/hMap.cmx
            - lib/coq/clib/hMap.cmi
            - lib/coq/clib/exninfo.cmx
            - lib/coq/clib/exninfo.cmi
            - lib/coq/clib/dyn.cmx
            - lib/coq/clib/dyn.cmi
            - lib/coq/clib/diff2.cmx
            - lib/coq/clib/diff2.cmi
            - lib/coq/clib/clib.cmxa
            - lib/coq/clib/clib.cma
            - lib/coq/clib/clib.a
            - lib/coq/clib/cUnix.cmx
            - lib/coq/clib/cUnix.cmi
            - lib/coq/clib/cThread.cmx
            - lib/coq/clib/cThread.cmi
            - lib/coq/clib/cString.cmx
            - lib/coq/clib/cString.cmi
            - lib/coq/clib/cStack.cmx
            - lib/coq/clib/cStack.cmi
            - lib/coq/clib/cSig.cmi
            - lib/coq/clib/cSet.cmx
            - lib/coq/clib/cSet.cmi
            - lib/coq/clib/cObj.cmx
            - lib/coq/clib/cObj.cmi
            - lib/coq/clib/cMap.cmx
            - lib/coq/clib/cMap.cmi
            - lib/coq/clib/cList.cmx
            - lib/coq/clib/cList.cmi
            - lib/coq/clib/cEphemeron.cmx
            - lib/coq/clib/cEphemeron.cmi
            - lib/coq/clib/cArray.cmx
            - lib/coq/clib/cArray.cmi
            - lib/coq/clib/bigint.cmx
            - lib/coq/clib/bigint.cmi
            - lib/coq/clib/backtrace.cmx
            - lib/coq/clib/backtrace.cmi
            - lib/coq/META
            - bin/votour
            - bin/coqtop.opt
            - bin/coqtacticworker.opt
            - bin/coqtacticworker.byte
            - bin/coqqueryworker.opt
            - bin/coqqueryworker.byte
            - bin/coqproofworker.opt
            - bin/coqproofworker.byte
            - bin/coqpp
            - bin/coqidetop.opt
            - bin/coqidetop
[NOTE] While removing coq.8.11.dev: not removing non-empty directories:
         - share/texmf/tex/latex/misc
         - lib/coq/vernac
         - lib/coq/user-contrib/Ltac2
         - lib/coq/toplevel
         - lib/coq/topbin
         - lib/coq/tools/coqdoc
         - lib/coq/theories/ZArith/.coq-native
         - lib/coq/theories/Wellfounded/.coq-native
         - lib/coq/theories/Vectors/.coq-native
         - lib/coq/theories/Unicode/.coq-native
         - lib/coq/theories/Structures/.coq-native
         - lib/coq/theories/Strings/.coq-native
         - lib/coq/theories/Sorting/.coq-native
         - lib/coq/theories/Sets/.coq-native
         - lib/coq/theories/Setoids/.coq-native
         - lib/coq/theories/Relations/.coq-native
         - lib/coq/theories/Reals/.coq-native
         - lib/coq/theories/QArith/.coq-native
         - lib/coq/theories/Program/.coq-native
         - lib/coq/theories/PArith/.coq-native
         - lib/coq/theories/Numbers/Natural/Peano/.coq-native
         - lib/coq/theories/Numbers/Natural/Binary/.coq-native
         - lib/coq/theories/Numbers/Natural/Abstract/.coq-native
         - lib/coq/theories/Numbers/NatInt/.coq-native
         - lib/coq/theories/Numbers/Integer/NatPairs/.coq-native
         - lib/coq/theories/Numbers/Integer/Binary/.coq-native
         - lib/coq/theories/Numbers/Integer/Abstract/.coq-native
         - lib/coq/theories/Numbers/Cyclic/ZModulo/.coq-native
         - lib/coq/theories/Numbers/Cyclic/Int63/.coq-native
         - lib/coq/theories/Numbers/Cyclic/Int31/.coq-native
         - lib/coq/theories/Numbers/Cyclic/Abstract/.coq-native
         - lib/coq/theories/Numbers/.coq-native
         - lib/coq/theories/NArith/.coq-native
         - lib/coq/theories/MSets/.coq-native
         - lib/coq/theories/Logic/.coq-native
         - lib/coq/theories/Lists/.coq-native
         - lib/coq/theories/Init/.coq-native
         - lib/coq/theories/Floats/.coq-native
         - lib/coq/theories/FSets/.coq-native
         - lib/coq/theories/Compat/.coq-native
         - lib/coq/theories/Classes/.coq-native
         - lib/coq/theories/Bool/.coq-native
         - lib/coq/theories/Arith/.coq-native
         - lib/coq/tactics
         - lib/coq/stm
         - lib/coq/proofs
         - lib/coq/printing
         - lib/coq/pretyping
         - lib/coq/plugins/syntax
         - lib/coq/plugins/ssrmatching/.coq-native
         - lib/coq/plugins/ssr/.coq-native
         - lib/coq/plugins/setoid_ring/.coq-native
         - lib/coq/plugins/rtauto/.coq-native
         - lib/coq/plugins/omega/.coq-native
         - lib/coq/plugins/nsatz/.coq-native
         - lib/coq/plugins/micromega/.coq-native
         - lib/coq/plugins/ltac/.coq-native
         - lib/coq/plugins/funind/.coq-native
         - lib/coq/plugins/firstorder
         - lib/coq/plugins/extraction/.coq-native
         - lib/coq/plugins/derive/.coq-native
         - lib/coq/plugins/cc
         - lib/coq/plugins/btauto/.coq-native
         - lib/coq/parsing
         - lib/coq/library
         - lib/coq/kernel/byterun
         - lib/coq/interp
         - lib/coq/gramlib/.pack
         - lib/coq/engine
         - lib/coq/dev
         - lib/coq/coqpp
         - lib/coq/config
         - lib/coq/clib
-> removed   coq.8.11.dev
Done.
# Run eval $(opam env) to update the current shell environment
The following dependencies couldn't be met:
  - coq-orb-stab -> coq-lin-alg >= dev
      no matching version
No solution found, exiting
The middle of the output is truncated (maximum 1000 lines)

Install dependencies

Command
true
Return code
0
Duration
0 s

Install

Command
true
Return code
0
Duration
0 s

Installation size

No files were installed.

Uninstall

Command
true
Return code
0
Missing removes
none
Wrong removes
none