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