WARNING: (guile-user): imported module (guix build utils) overrides core binding `delete'
starting phase `set-SOURCE-DATE-EPOCH'
phase `set-SOURCE-DATE-EPOCH' succeeded after 0.0 seconds
starting phase `set-paths'
environment variable `PATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/bin:/gnu/store/n3gp6sh4fb3ar05mmkwp2avn55sn9mj1-which-2.21/bin:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin:/gnu/store/am3imbjafa1wdvw9j6qabrxc09w169lz-tar-1.32/bin:/gnu/store/chqjscapsg928dy8pg6yrdhw3ypk8c9x-gzip-1.10/bin:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/bin:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/bin:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/bin:/gnu/store/m8fnsfqs18c3srjiaw4frqadb9rqsq16-diffutils-3.7/bin:/gnu/store/2cfnrxy8icrz3sxfn86k0klmvsnj1n82-patch-2.7.6/bin:/gnu/store/0bmzacdzdhi41kkjbsq7iakwjzxkv6fm-findutils-4.7.0/bin:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/bin:/gnu/store/qy7gpiba7s7ylpfxaay6i76rk892j52n-sed-4.8/bin:/gnu/store/74d5jq5sj2fhy5j0j07jqdclf8nyxgqn-grep-3.4/bin:/gnu/store/wy177cwa387g9kaf3ss716d4fhzb21wx-coreutils-8.32/bin:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/bin:/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin:/gnu/store/y4iy1jvfq07gxynkb9jl1f69jmy349vi-ld-wrapper-0/bin:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/bin:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/bin:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/sbin'
environment variable `OCAMLPATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/stublibs'
environment variable `COQPATH' unset
environment variable `COQLIB' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/coq'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/include:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/include:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/include:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/include:/gnu/store/wsxnp4k7mp7b705kxp94j7hs8as5fmsl-make-4.3/include:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/include:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include/c++:/gnu/store/z8954h4nvgxwcyy2in8c1l11g199m2yb-gcc-7.5.0/include:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/include:/gnu/store/72z9rxrrmfw1xx9gf27jm2s8h5h0fkh0-linux-libre-headers-5.4.20/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/0n43gkkd4565sii8qv31asjj9b4n3rqy-ocaml-4.11.1/lib:/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib:/gnu/store/k3n5jh5579g2b17qmd2w89z2fy45pmr3-bzip2-1.0.8/lib:/gnu/store/k8ksi57ghm301zr0v7aq2vl2fa8hxfqi-xz-5.2.4/lib:/gnu/store/5ckix15mw8r509g68fbm7rla51lmd2zq-file-5.38/lib:/gnu/store/x9qzb42hmzszg9y16m1gbz3vv54yyi00-gawk-5.0.1/lib:/gnu/store/1iwrsjwmhcdifc8i3v7qdr59k6gq4z24-binutils-2.34/lib:/gnu/store/llkv94k15spryi6zf0gjm0fp7m8k3i8g-glibc-2.31/lib:/gnu/store/m4l52mw8m0amgy4j129z5j0syryb7pkg-glibc-2.31-static/lib:/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-glibc-utf8-locales-2.31/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/vispxhcwmvasm225pm373jhfn21q1sa1-glibc-utf8-locales-2.31/lib/locale'
phase `set-paths' succeeded after 0.1 seconds
starting phase `install-locale'
using 'en_US.utf8' locale for category "LC_ALL"
phase `install-locale' succeeded after 0.0 seconds
starting phase `unpack'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.gitattributes' -> `./.gitattributes'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.gitlab-ci.yml' -> `./.gitlab-ci.yml'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.mailmap' -> `./.mailmap'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/CHANGELOG.md' -> `./CHANGELOG.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/CONTRIBUTING.md' -> `./CONTRIBUTING.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/INSTALL.md' -> `./INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-algebra.opam' -> `./coq-mathcomp-algebra.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-character.opam' -> `./coq-mathcomp-character.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-field.opam' -> `./coq-mathcomp-field.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-fingroup.opam' -> `./coq-mathcomp-fingroup.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-solvable.opam' -> `./coq-mathcomp-solvable.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/coq-mathcomp-ssreflect.opam' -> `./coq-mathcomp-ssreflect.opam'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/default.nix' -> `./default.nix'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.dockerignore' -> `./.dockerignore'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/AUTHORS' -> `./AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/CHANGELOG_UNRELEASED.md' -> `./CHANGELOG_UNRELEASED.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/CeCILL-B' -> `./CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/Dockerfile' -> `./Dockerfile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/Dockerfile.make' -> `./Dockerfile.make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/README.md' -> `./README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/config.nix' -> `./config.nix'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/package.nix' -> `./package.nix'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/Make' -> `./mathcomp/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/Make.test-suite' -> `./mathcomp/Make.test-suite'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/Makefile.common' -> `./mathcomp/Makefile.common'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/Makefile.test-suite.coq.local' -> `./mathcomp/Makefile.test-suite.coq.local'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/_CoqProject' -> `./mathcomp/_CoqProject'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/Makefile' -> `./mathcomp/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/imset2_finset.v' -> `./mathcomp/test_suite/imset2_finset.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/imset2_finset.v.out' -> `./mathcomp/test_suite/imset2_finset.v.out'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/imset2_gproduct.v' -> `./mathcomp/test_suite/imset2_gproduct.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/imset2_gproduct.v.out' -> `./mathcomp/test_suite/imset2_gproduct.v.out'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/output.v' -> `./mathcomp/test_suite/output.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/output.v.out' -> `./mathcomp/test_suite/output.v.out'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/output.v.out.8.7' -> `./mathcomp/test_suite/output.v.out.8.7'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/output.v.out.8.9' -> `./mathcomp/test_suite/output.v.out.8.9'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/test_guard.v' -> `./mathcomp/test_suite/test_guard.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/test_intro_rw.v' -> `./mathcomp/test_suite/test_intro_rw.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/test_regular_conv.v' -> `./mathcomp/test_suite/test_regular_conv.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/output.v.out.8.8' -> `./mathcomp/test_suite/output.v.out.8.8'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/test_suite/test_ssrAC.v' -> `./mathcomp/test_suite/test_ssrAC.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/Make' -> `./mathcomp/ssreflect/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/bigop.v' -> `./mathcomp/ssreflect/bigop.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/binomial.v' -> `./mathcomp/ssreflect/binomial.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/choice.v' -> `./mathcomp/ssreflect/choice.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/div.v' -> `./mathcomp/ssreflect/div.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/eqtype.v' -> `./mathcomp/ssreflect/eqtype.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/finfun.v' -> `./mathcomp/ssreflect/finfun.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/fingraph.v' -> `./mathcomp/ssreflect/fingraph.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/finset.v' -> `./mathcomp/ssreflect/finset.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/fintype.v' -> `./mathcomp/ssreflect/fintype.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/generic_quotient.v' -> `./mathcomp/ssreflect/generic_quotient.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/order.v' -> `./mathcomp/ssreflect/order.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/path.v' -> `./mathcomp/ssreflect/path.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/prime.v' -> `./mathcomp/ssreflect/prime.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/seq.v' -> `./mathcomp/ssreflect/seq.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrAC.v' -> `./mathcomp/ssreflect/ssrAC.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrbool.v' -> `./mathcomp/ssreflect/ssrbool.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssreflect.v' -> `./mathcomp/ssreflect/ssreflect.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrfun.v' -> `./mathcomp/ssreflect/ssrfun.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrnat.v' -> `./mathcomp/ssreflect/ssrnat.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/tuple.v' -> `./mathcomp/ssreflect/tuple.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/AUTHORS' -> `./mathcomp/ssreflect/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/CeCILL-B' -> `./mathcomp/ssreflect/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/INSTALL.md' -> `./mathcomp/ssreflect/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/INSTALL.pg' -> `./mathcomp/ssreflect/INSTALL.pg'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/Makefile' -> `./mathcomp/ssreflect/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/README.md' -> `./mathcomp/ssreflect/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/all_ssreflect.v' -> `./mathcomp/ssreflect/all_ssreflect.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/pg-ssr.el' -> `./mathcomp/ssreflect/pg-ssr.el'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrmatching.v' -> `./mathcomp/ssreflect/ssrmatching.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/ssreflect/ssrnotations.v' -> `./mathcomp/ssreflect/ssrnotations.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/Make' -> `./mathcomp/solvable/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/abelian.v' -> `./mathcomp/solvable/abelian.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/alt.v' -> `./mathcomp/solvable/alt.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/center.v' -> `./mathcomp/solvable/center.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/commutator.v' -> `./mathcomp/solvable/commutator.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/cyclic.v' -> `./mathcomp/solvable/cyclic.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/extraspecial.v' -> `./mathcomp/solvable/extraspecial.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/extremal.v' -> `./mathcomp/solvable/extremal.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/finmodule.v' -> `./mathcomp/solvable/finmodule.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/gfunctor.v' -> `./mathcomp/solvable/gfunctor.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/gseries.v' -> `./mathcomp/solvable/gseries.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/hall.v' -> `./mathcomp/solvable/hall.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/jordanholder.v' -> `./mathcomp/solvable/jordanholder.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/maximal.v' -> `./mathcomp/solvable/maximal.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/nilpotent.v' -> `./mathcomp/solvable/nilpotent.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/pgroup.v' -> `./mathcomp/solvable/pgroup.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/primitive_action.v' -> `./mathcomp/solvable/primitive_action.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/sylow.v' -> `./mathcomp/solvable/sylow.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/AUTHORS' -> `./mathcomp/solvable/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/CeCILL-B' -> `./mathcomp/solvable/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/INSTALL.md' -> `./mathcomp/solvable/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/Makefile' -> `./mathcomp/solvable/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/README.md' -> `./mathcomp/solvable/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/all_solvable.v' -> `./mathcomp/solvable/all_solvable.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/burnside_app.v' -> `./mathcomp/solvable/burnside_app.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/solvable/frobenius.v' -> `./mathcomp/solvable/frobenius.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/Make' -> `./mathcomp/fingroup/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/action.v' -> `./mathcomp/fingroup/action.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/automorphism.v' -> `./mathcomp/fingroup/automorphism.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/fingroup.v' -> `./mathcomp/fingroup/fingroup.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/gproduct.v' -> `./mathcomp/fingroup/gproduct.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/morphism.v' -> `./mathcomp/fingroup/morphism.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/perm.v' -> `./mathcomp/fingroup/perm.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/presentation.v' -> `./mathcomp/fingroup/presentation.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/quotient.v' -> `./mathcomp/fingroup/quotient.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/AUTHORS' -> `./mathcomp/fingroup/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/CeCILL-B' -> `./mathcomp/fingroup/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/INSTALL.md' -> `./mathcomp/fingroup/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/Makefile' -> `./mathcomp/fingroup/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/README.md' -> `./mathcomp/fingroup/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/fingroup/all_fingroup.v' -> `./mathcomp/fingroup/all_fingroup.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/Make' -> `./mathcomp/field/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/algC.v' -> `./mathcomp/field/algC.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/algebraics_fundamentals.v' -> `./mathcomp/field/algebraics_fundamentals.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/algnum.v' -> `./mathcomp/field/algnum.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/closed_field.v' -> `./mathcomp/field/closed_field.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/cyclotomic.v' -> `./mathcomp/field/cyclotomic.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/falgebra.v' -> `./mathcomp/field/falgebra.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/fieldext.v' -> `./mathcomp/field/fieldext.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/finfield.v' -> `./mathcomp/field/finfield.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/galois.v' -> `./mathcomp/field/galois.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/separable.v' -> `./mathcomp/field/separable.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/AUTHORS' -> `./mathcomp/field/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/CeCILL-B' -> `./mathcomp/field/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/INSTALL.md' -> `./mathcomp/field/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/Makefile' -> `./mathcomp/field/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/README.md' -> `./mathcomp/field/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/field/all_field.v' -> `./mathcomp/field/all_field.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/Make' -> `./mathcomp/character/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/character.v' -> `./mathcomp/character/character.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/classfun.v' -> `./mathcomp/character/classfun.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/inertia.v' -> `./mathcomp/character/inertia.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/integral_char.v' -> `./mathcomp/character/integral_char.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/mxabelem.v' -> `./mathcomp/character/mxabelem.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/mxrepresentation.v' -> `./mathcomp/character/mxrepresentation.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/vcharacter.v' -> `./mathcomp/character/vcharacter.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/AUTHORS' -> `./mathcomp/character/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/CeCILL-B' -> `./mathcomp/character/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/INSTALL.md' -> `./mathcomp/character/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/Makefile' -> `./mathcomp/character/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/README.md' -> `./mathcomp/character/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/character/all_character.v' -> `./mathcomp/character/all_character.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/all/Makefile' -> `./mathcomp/all/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/all/all.v' -> `./mathcomp/all/all.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/AUTHORS' -> `./mathcomp/algebra/AUTHORS'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/CeCILL-B' -> `./mathcomp/algebra/CeCILL-B'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/INSTALL.md' -> `./mathcomp/algebra/INSTALL.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/Make' -> `./mathcomp/algebra/Make'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/countalg.v' -> `./mathcomp/algebra/countalg.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/finalg.v' -> `./mathcomp/algebra/finalg.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/intdiv.v' -> `./mathcomp/algebra/intdiv.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/interval.v' -> `./mathcomp/algebra/interval.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/matrix.v' -> `./mathcomp/algebra/matrix.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/mxalgebra.v' -> `./mathcomp/algebra/mxalgebra.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/mxpoly.v' -> `./mathcomp/algebra/mxpoly.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/poly.v' -> `./mathcomp/algebra/poly.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/polyXY.v' -> `./mathcomp/algebra/polyXY.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/polydiv.v' -> `./mathcomp/algebra/polydiv.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/rat.v' -> `./mathcomp/algebra/rat.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/ssralg.v' -> `./mathcomp/algebra/ssralg.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/ssrint.v' -> `./mathcomp/algebra/ssrint.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/ssrnum.v' -> `./mathcomp/algebra/ssrnum.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/vector.v' -> `./mathcomp/algebra/vector.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/zmodp.v' -> `./mathcomp/algebra/zmodp.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/Makefile' -> `./mathcomp/algebra/Makefile'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/README.md' -> `./mathcomp/algebra/README.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/all_algebra.v' -> `./mathcomp/algebra/all_algebra.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/fraction.v' -> `./mathcomp/algebra/fraction.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/mathcomp/algebra/ring_quotient.v' -> `./mathcomp/algebra/ring_quotient.v'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/ANNOUNCE-1.6.md' -> `./etc/ANNOUNCE-1.6.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/ANNOUNCE-github.md' -> `./etc/ANNOUNCE-github.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/NOTICE' -> `./etc/NOTICE'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/buildlibgraph' -> `./etc/buildlibgraph'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/win-installer.nsi' -> `./etc/win-installer.nsi'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/utils/hierarchy.ml' -> `./etc/utils/hierarchy.ml'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/utils/builddoc_lib.sh' -> `./etc/utils/builddoc_lib.sh'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/utils/dependtodot.ml' -> `./etc/utils/dependtodot.ml'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/utils/packager' -> `./etc/utils/packager'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/artwork/coqdoc.css' -> `./etc/artwork/coqdoc.css'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/etc/artwork/jc.png' -> `./etc/artwork/jc.png'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/docs/index.html' -> `./docs/index.html'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.github/pull_request_template.md' -> `./.github/pull_request_template.md'
`/gnu/store/y4by1imfdjsnzimf6kpdrar6g5v8y9bi-coq-mathcomp-1.12.0-checkout/.github/workflows/nix.yml' -> `./.github/workflows/nix.yml'
phase `unpack' succeeded after 0.1 seconds
starting phase `bootstrap'
no 'configure.ac' or anything like that, doing nothing
phase `bootstrap' succeeded after 0.0 seconds
starting phase `patch-usr-bin-file'
phase `patch-usr-bin-file' succeeded after 0.0 seconds
starting phase `patch-source-shebangs'
patch-shebang: ./etc/buildlibgraph: warning: no binary for interpreter `lua' found in $PATH
patch-shebang: ./etc/utils/packager: changing `/bin/bash' to `/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/bash'
phase `patch-source-shebangs' succeeded after 0.0 seconds
starting phase `patch-generated-file-shebangs'
patch-shebang: ./etc/buildlibgraph: warning: no binary for interpreter `lua' found in $PATH
phase `patch-generated-file-shebangs' succeeded after 0.0 seconds
starting phase `chdir'
phase `chdir' succeeded after 0.0 seconds
starting phase `build'
/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin/coq_makefile  -f Make -o Makefile.coq
make -f Makefile.coq --no-print-directory
COQDEP VFILES
COQC ssreflect/ssreflect.v
COQC ssreflect/ssrnotations.v
COQC ssreflect/ssrmatching.v
COQC ssreflect/ssrfun.v
COQC ssreflect/ssrbool.v
File "./ssreflect/ssrbool.v", line 42, characters 0-128:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 42, characters 0-128:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 45, characters 0-152:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 45, characters 0-152:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 49, characters 0-192:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 49, characters 0-192:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 52, characters 0-172:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 52, characters 0-172:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 55, characters 0-165:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 55, characters 0-165:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 58, characters 0-144:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/ssrbool.v", line 58, characters 0-144:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
COQC ssreflect/eqtype.v
File "./ssreflect/eqtype.v", line 200, characters 0-35:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/eqtype.v", line 504, characters 0-213:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/eqtype.v", line 509, characters 0-294:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
COQC ssreflect/ssrnat.v
File "./ssreflect/ssrnat.v", line 114, characters 0-58:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/ssrnat.v", line 331, characters 0-26:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/ssrnat.v", line 335, characters 0-27:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/ssrnat.v", line 365, characters 0-40:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/ssrnat.v", line 402, characters 0-25:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/seq.v
File "./ssreflect/seq.v", line 1512, characters 0-93:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/seq.v", line 1864, characters 0-30:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/seq.v", line 2233, characters 0-32:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/seq.v", line 2369, characters 0-161:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2373, characters 0-187:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2377, characters 0-129:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2380, characters 0-150:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2384, characters 0-130:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2387, characters 0-144:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2390, characters 0-138:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 2393, characters 0-158:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3230, characters 0-224:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3230, characters 0-224:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3235, characters 0-179:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3235, characters 0-179:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3238, characters 0-187:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3238, characters 0-187:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3241, characters 0-171:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/seq.v", line 3241, characters 0-171:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
COQC ssreflect/div.v
COQC ssreflect/choice.v
COQC ssreflect/path.v
File "./ssreflect/div.v", line 371, characters 0-58:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/div.v", line 507, characters 0-47:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/fintype.v
File "./ssreflect/fintype.v", line 283, characters 0-121:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 285, characters 0-112:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 288, characters 0-89:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 294, characters 0-91:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 296, characters 0-147:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 299, characters 0-113:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 301, characters 0-124:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 303, characters 0-112:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 305, characters 0-158:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 308, characters 0-121:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 310, characters 0-171:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 313, characters 0-124:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 365, characters 0-71:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 366, characters 0-79:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 923, characters 0-31:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/fintype.v", line 1131, characters 0-167:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 1134, characters 0-133:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 1136, characters 0-194:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 1140, characters 0-112:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/fintype.v", line 1813, characters 0-28:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/tuple.v
COQC ssreflect/generic_quotient.v
COQC ssreflect/fingraph.v
File "./ssreflect/generic_quotient.v", line 497, characters 0-31:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/fingraph.v", line 226, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/finfun.v
File "./ssreflect/finfun.v", line 126, characters 0-100:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./ssreflect/finfun.v", line 129, characters 0-134:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
COQC ssreflect/bigop.v
File "./ssreflect/fingraph.v", line 850, characters 0-60:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/bigop.v", line 576, characters 0-35:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/prime.v
COQC ssreflect/finset.v
COQC ssreflect/ssrAC.v
File "./ssreflect/finset.v", line 262, characters 0-28:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/prime.v", line 363, characters 0-40:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/prime.v", line 504, characters 0-42:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/prime.v", line 644, characters 0-32:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/finset.v", line 1023, characters 0-33:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/prime.v", line 1255, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC ssreflect/binomial.v
COQC ssreflect/order.v
COQC fingroup/fingroup.v
File "./fingroup/fingroup.v", line 494, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC algebra/ssralg.v
File "./fingroup/fingroup.v", line 1824, characters 0-60:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./fingroup/fingroup.v", line 1825, characters 0-62:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./fingroup/fingroup.v", line 1826, characters 0-67:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./fingroup/fingroup.v", line 1892, characters 0-30:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3241, characters 0-52:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3242, characters 0-52:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3434, characters 0-64:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3936, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3937, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3938, characters 0-32:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./ssreflect/order.v", line 3939, characters 0-35:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./fingroup/fingroup.v", line 2985, characters 0-61:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./fingroup/fingroup.v", line 2986, characters 0-62:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC fingroup/morphism.v
COQC ssreflect/all_ssreflect.v
COQC algebra/ring_quotient.v
COQC fingroup/perm.v
COQC fingroup/presentation.v
COQC algebra/countalg.v
COQC algebra/poly.v
COQC fingroup/automorphism.v
File "./fingroup/automorphism.v", line 449, characters 0-30:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC fingroup/quotient.v
COQC algebra/ssrnum.v
COQC algebra/polydiv.v
COQC fingroup/action.v
File "./algebra/ssrnum.v", line 1577, characters 0-45:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/ssrnum.v", line 1578, characters 0-65:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/polydiv.v", line 919, characters 0-39:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/ssrnum.v", line 3511, characters 0-61:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/ssrnum.v", line 3926, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/polydiv.v", line 2358, characters 0-82:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/polydiv.v", line 2359, characters 0-26:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC algebra/ssrint.v
COQC algebra/interval.v
COQC algebra/finalg.v
COQC fingroup/gproduct.v
COQC algebra/zmodp.v
COQC algebra/fraction.v
COQC algebra/matrix.v
File "./algebra/fraction.v", line 297, characters 0-33:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC algebra/rat.v
File "./algebra/rat.v", line 56, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/rat.v", line 64, characters 0-30:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/rat.v", line 368, characters 0-48:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/matrix.v", line 2599, characters 0-88:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/matrix.v", line 2601, characters 0-88:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/matrix.v", line 2603, characters 0-84:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/matrix.v", line 2605, characters 0-84:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./algebra/matrix.v", line 3147, characters 0-50:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC solvable/cyclic.v
COQC solvable/gfunctor.v
COQC fingroup/all_fingroup.v
COQC algebra/mxalgebra.v
COQC solvable/commutator.v
COQC solvable/pgroup.v
COQC solvable/center.v
File "./algebra/mxalgebra.v", line 2192, characters 0-31:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC solvable/finmodule.v
COQC solvable/gseries.v
COQC algebra/mxpoly.v
COQC algebra/vector.v
COQC solvable/nilpotent.v
COQC solvable/primitive_action.v
COQC solvable/jordanholder.v
COQC solvable/sylow.v
File "./algebra/vector.v", line 1227, characters 0-26:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC solvable/burnside_app.v
COQC solvable/abelian.v
COQC solvable/alt.v
COQC algebra/polyXY.v
COQC algebra/intdiv.v
COQC field/closed_field.v
File "./field/closed_field.v", line 88, characters 0-99:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File "./algebra/intdiv.v", line 327, characters 0-58:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC field/falgebra.v
COQC character/mxrepresentation.v
COQC solvable/maximal.v
COQC algebra/all_algebra.v
COQC field/fieldext.v
COQC solvable/hall.v
COQC solvable/extremal.v
COQC field/separable.v
COQC solvable/frobenius.v
COQC field/galois.v
COQC solvable/extraspecial.v
COQC character/mxabelem.v
COQC field/algebraics_fundamentals.v
COQC solvable/all_solvable.v
COQC field/algC.v
File "./field/algC.v", line 1249, characters 0-87:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./field/algC.v", line 1250, characters 0-57:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC field/cyclotomic.v
COQC field/algnum.v
COQC field/finfield.v
File "./field/algnum.v", line 554, characters 0-32:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./field/algnum.v", line 706, characters 0-32:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
File "./field/algnum.v", line 743, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC field/all_field.v
COQC character/classfun.v
File "./character/classfun.v", line 758, characters 0-29:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality is therefore deprecated. It is recommended to
use "export" whenever possible. [deprecated-hint-without-locality,deprecated]
COQC character/character.v
COQC character/inertia.v
COQC character/integral_char.v
COQC character/vcharacter.v
COQC character/all_character.v
COQC all/all.v
phase `build' succeeded after 1247.7 seconds
starting phase `check'
test suite not run
phase `check' succeeded after 0.0 seconds
starting phase `install'
INSTALL algebra/all_algebra.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/finalg.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/countalg.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/fraction.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/intdiv.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/interval.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/matrix.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxalgebra.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxpoly.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polydiv.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/poly.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polyXY.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/rat.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ring_quotient.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssralg.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrint.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrnum.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/vector.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/zmodp.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL all/all.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//all
INSTALL character/all_character.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/character.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/classfun.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/inertia.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/integral_char.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxabelem.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxrepresentation.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/vcharacter.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL field/algC.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algebraics_fundamentals.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algnum.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/all_field.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/closed_field.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/cyclotomic.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/falgebra.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/fieldext.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/finfield.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/galois.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/separable.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL fingroup/action.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/all_fingroup.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/automorphism.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/fingroup.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/gproduct.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/morphism.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/perm.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/presentation.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/quotient.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL solvable/abelian.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/all_solvable.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/alt.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/burnside_app.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/center.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/commutator.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/cyclic.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extraspecial.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extremal.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/finmodule.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/frobenius.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gfunctor.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gseries.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/hall.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/jordanholder.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/maximal.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/nilpotent.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/pgroup.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/primitive_action.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/sylow.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL ssreflect/all_ssreflect.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/bigop.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/binomial.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/choice.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/div.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/eqtype.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finfun.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fingraph.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finset.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fintype.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/generic_quotient.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/order.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/path.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/prime.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/seq.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrAC.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrbool.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssreflect.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrfun.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnat.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnotations.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrmatching.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/tuple.vo /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL algebra/all_algebra.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/finalg.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/countalg.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/fraction.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/intdiv.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/interval.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/matrix.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxalgebra.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxpoly.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polydiv.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/poly.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polyXY.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/rat.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ring_quotient.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssralg.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrint.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrnum.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/vector.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/zmodp.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL all/all.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//all
INSTALL character/all_character.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/character.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/classfun.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/inertia.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/integral_char.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxabelem.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxrepresentation.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/vcharacter.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL field/algC.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algebraics_fundamentals.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algnum.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/all_field.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/closed_field.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/cyclotomic.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/falgebra.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/fieldext.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/finfield.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/galois.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/separable.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL fingroup/action.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/all_fingroup.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/automorphism.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/fingroup.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/gproduct.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/morphism.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/perm.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/presentation.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/quotient.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL solvable/abelian.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/all_solvable.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/alt.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/burnside_app.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/center.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/commutator.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/cyclic.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extraspecial.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extremal.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/finmodule.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/frobenius.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gfunctor.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gseries.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/hall.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/jordanholder.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/maximal.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/nilpotent.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/pgroup.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/primitive_action.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/sylow.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL ssreflect/all_ssreflect.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/bigop.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/binomial.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/choice.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/div.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/eqtype.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finfun.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fingraph.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finset.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fintype.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/generic_quotient.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/order.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/path.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/prime.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/seq.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrAC.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrbool.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssreflect.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrfun.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnat.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnotations.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrmatching.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/tuple.v /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL algebra/all_algebra.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/finalg.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/countalg.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/fraction.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/intdiv.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/interval.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/matrix.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxalgebra.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/mxpoly.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polydiv.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/poly.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/polyXY.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/rat.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ring_quotient.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssralg.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrint.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/ssrnum.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/vector.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL algebra/zmodp.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//algebra
INSTALL all/all.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//all
INSTALL character/all_character.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/character.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/classfun.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/inertia.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/integral_char.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxabelem.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/mxrepresentation.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL character/vcharacter.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//character
INSTALL field/algC.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algebraics_fundamentals.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/algnum.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/all_field.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/closed_field.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/cyclotomic.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/falgebra.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/fieldext.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/finfield.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/galois.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL field/separable.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//field
INSTALL fingroup/action.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/all_fingroup.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/automorphism.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/fingroup.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/gproduct.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/morphism.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/perm.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/presentation.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL fingroup/quotient.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//fingroup
INSTALL solvable/abelian.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/all_solvable.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/alt.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/burnside_app.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/center.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/commutator.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/cyclic.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extraspecial.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/extremal.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/finmodule.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/frobenius.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gfunctor.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/gseries.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/hall.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/jordanholder.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/maximal.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/nilpotent.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/pgroup.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/primitive_action.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL solvable/sylow.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//solvable
INSTALL ssreflect/all_ssreflect.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/bigop.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/binomial.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/choice.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/div.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/eqtype.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finfun.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fingraph.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/finset.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/fintype.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/generic_quotient.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/order.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/path.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/prime.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/seq.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrAC.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrbool.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssreflect.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrfun.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnat.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrnotations.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/ssrmatching.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
INSTALL ssreflect/tuple.glob /gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib/coq//user-contrib/mathcomp//ssreflect
make[1]: Entering directory '/tmp/guix-build-coq-mathcomp-1.12.0.drv-0/source/mathcomp'
make[1]: Leaving directory '/tmp/guix-build-coq-mathcomp-1.12.0.drv-0/source/mathcomp'
phase `install' succeeded after 5.3 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib" with "strip" and flags ("--strip-debug" "--enable-deterministic-archives")
phase `strip' succeeded after 0.1 seconds
starting phase `validate-runpath'
validating RUNPATH of 0 binaries in "/gnu/store/zwk16jnyg8fpbwxang5wfn9377hhk1pw-coq-mathcomp-1.12.0/lib"...
phase `validate-runpath' succeeded after 0.0 seconds
starting phase `validate-documentation-location'
phase `validate-documentation-location' succeeded after 0.0 seconds
starting phase `delete-info-dir-file'
phase `delete-info-dir-file' succeeded after 0.0 seconds
starting phase `patch-dot-desktop-files'
phase `patch-dot-desktop-files' succeeded after 0.0 seconds
starting phase `install-license-files'
installing 0 license files from '.'
phase `install-license-files' succeeded after 0.0 seconds
starting phase `reset-gzip-timestamps'
phase `reset-gzip-timestamps' succeeded after 0.0 seconds
starting phase `compress-documentation'
phase `compress-documentation' succeeded after 0.0 seconds