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/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/bin:/gnu/store/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/bin:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/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:/gnu/store/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/lib/ocaml:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/lib/ocaml/site-lib'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/jaryidlibxa6hbymx0qs7ndlbdrr8g7p-coq-8.13.2/lib/ocaml/site-lib/stublibs:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/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/6h907snwcc3gjcxi6b41wx8nzim3390q-camlp5-7.13/lib:/gnu/store/krsbvgjjc67wv646p06caxi1g80vdg16-ocaml-zarith-1.12/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/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/siteexamples.sh' -> `./siteexamples.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/_HoTTProject' -> `./_HoTTProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/README.md' -> `./README.md'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/equations.opam' -> `./equations.opam'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile' -> `./Makefile'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/configure.sh' -> `./configure.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Gemfile' -> `./Gemfile'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/.travis.yml' -> `./.travis.yml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.local' -> `./Makefile.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/README.dev' -> `./README.dev'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/TODO' -> `./TODO'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/buildHoTT.sh' -> `./buildHoTT.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.coq.local' -> `./Makefile.coq.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/makedoc.sh' -> `./makedoc.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/dune-project' -> `./dune-project'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.HoTT.local' -> `./Makefile.HoTT.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/principles_proofs.ml' -> `./src/principles_proofs.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/depelim.mli' -> `./src/depelim.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations_common.mli' -> `./src/equations_common.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/principles_proofs.mli' -> `./src/principles_proofs.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/sigma_types.mli' -> `./src/sigma_types.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations.ml' -> `./src/equations.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/g_equations.mlg' -> `./src/g_equations.mlg'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/splitting.mli' -> `./src/splitting.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations_common.ml' -> `./src/equations_common.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/dune' -> `./src/dune'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/ederive.ml' -> `./src/ederive.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/covering.ml' -> `./src/covering.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/principles.ml' -> `./src/principles.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/simplify.mli' -> `./src/simplify.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/sigma_types.ml' -> `./src/sigma_types.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/noconf.mli' -> `./src/noconf.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/extra_tactics.mli' -> `./src/extra_tactics.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/noconf_hom.ml' -> `./src/noconf_hom.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations_plugin.mllib' -> `./src/equations_plugin.mllib'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/noconf_hom.mli' -> `./src/noconf_hom.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/syntax.mli' -> `./src/syntax.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/ederive.mli' -> `./src/ederive.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/subterm.ml' -> `./src/subterm.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations.mli' -> `./src/equations.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/splitting.ml' -> `./src/splitting.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/extra_tactics.ml' -> `./src/extra_tactics.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/context_map.ml' -> `./src/context_map.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/eqdec.ml' -> `./src/eqdec.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/subterm.mli' -> `./src/subterm.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/syntax.ml' -> `./src/syntax.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/principles.mli' -> `./src/principles.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/noconf.ml' -> `./src/noconf.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/eqdec.mli' -> `./src/eqdec.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/context_map.mli' -> `./src/context_map.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/equations_plugin_mod.ml' -> `./src/equations_plugin_mod.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/simplify.ml' -> `./src/simplify.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/covering.mli' -> `./src/covering.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/depelim.ml' -> `./src/depelim.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/dev/include' -> `./dev/include'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/.github/workflows/build.yml' -> `./.github/workflows/build.yml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/noconf_hom.v' -> `./test-suite/noconf_hom.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/f91.v' -> `./test-suite/f91.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/interval.v' -> `./test-suite/interval.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/univpoly.v' -> `./test-suite/univpoly.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/rec.v' -> `./test-suite/rec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/terms.v' -> `./test-suite/terms.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/cfold.v' -> `./test-suite/cfold.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/innacs.v' -> `./test-suite/innacs.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/fle_trans.v' -> `./test-suite/fle_trans.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/square_elim.v' -> `./test-suite/square_elim.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/Noconfinv.v' -> `./test-suite/Noconfinv.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/LogicType.v' -> `./test-suite/LogicType.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/noconf_noK_fin.v' -> `./test-suite/noconf_noK_fin.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/daaa.v' -> `./test-suite/daaa.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/le.v' -> `./test-suite/le.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestfixnorec.v' -> `./test-suite/nestfixnorec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/gcd.v' -> `./test-suite/gcd.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/wfnocycle.v' -> `./test-suite/wfnocycle.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/rose.v' -> `./test-suite/rose.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/agda_1775_full.v' -> `./test-suite/agda_1775_full.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/agda_1408.v' -> `./test-suite/agda_1408.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedwhererec.v' -> `./test-suite/nestedwhererec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedrec.v' -> `./test-suite/nestedrec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/tabareau_vec.v' -> `./test-suite/tabareau_vec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/ack.v' -> `./test-suite/ack.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/scope_noK.v' -> `./test-suite/scope_noK.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/pattern_lambdas.v' -> `./test-suite/pattern_lambdas.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/noconf_simplify.v' -> `./test-suite/noconf_simplify.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/mutrec_enc.v' -> `./test-suite/mutrec_enc.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/mutrec.v' -> `./test-suite/mutrec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/scope.v' -> `./test-suite/scope.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/agda_1775.v' -> `./test-suite/agda_1775.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/letred.v' -> `./test-suite/letred.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/noconf_noK.v' -> `./test-suite/noconf_noK.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/telescopes.v' -> `./test-suite/telescopes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/telescopes_nonempty.v' -> `./test-suite/telescopes_nonempty.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/eqdec_error.v' -> `./test-suite/eqdec_error.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/yves.v' -> `./test-suite/yves.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/Basics.v' -> `./test-suite/Basics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/divmod.v' -> `./test-suite/divmod.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedwhererecwith.v' -> `./test-suite/nestedwhererecwith.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/Noconflet.v' -> `./test-suite/Noconflet.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/DataStruct.v' -> `./test-suite/DataStruct.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/fin.v' -> `./test-suite/fin.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/_CoqProject' -> `./test-suite/_CoqProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/Below.v' -> `./test-suite/Below.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/zoe.v' -> `./test-suite/zoe.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedwfrec.v' -> `./test-suite/nestedwfrec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/depelim.v' -> `./test-suite/depelim.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/smolka_inj_K2.v' -> `./test-suite/smolka_inj_K2.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedrec2.v' -> `./test-suite/nestedrec2.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/BasicsDec.v' -> `./test-suite/BasicsDec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nestedobls.v' -> `./test-suite/nestedobls.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/BasicsHoTT.v' -> `./test-suite/BasicsHoTT.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/mfix.v' -> `./test-suite/mfix.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nocycle.v' -> `./test-suite/nocycle.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/local_where.v' -> `./test-suite/local_where.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/notations.v' -> `./test-suite/notations.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nolam.v' -> `./test-suite/nolam.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/nocycle_def.v' -> `./test-suite/nocycle_def.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue252.v' -> `./test-suite/issues/issue252.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue96.v' -> `./test-suite/issues/issue96.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue25.v' -> `./test-suite/issues/issue25.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue172.v' -> `./test-suite/issues/issue172.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue246.v' -> `./test-suite/issues/issue246.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue7.v' -> `./test-suite/issues/issue7.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue66.v' -> `./test-suite/issues/issue66.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue70.v' -> `./test-suite/issues/issue70.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue63.v' -> `./test-suite/issues/issue63.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue116.v' -> `./test-suite/issues/issue116.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue340.v' -> `./test-suite/issues/issue340.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue98.v' -> `./test-suite/issues/issue98.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue106.v' -> `./test-suite/issues/issue106.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue200.v' -> `./test-suite/issues/issue200.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue112.v' -> `./test-suite/issues/issue112.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue85.v' -> `./test-suite/issues/issue85.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue75.v' -> `./test-suite/issues/issue75.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue113.v' -> `./test-suite/issues/issue113.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue105.v' -> `./test-suite/issues/issue105.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue95_1.v' -> `./test-suite/issues/issue95_1.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue95_2.v' -> `./test-suite/issues/issue95_2.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue249.v' -> `./test-suite/issues/issue249.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue84.v' -> `./test-suite/issues/issue84.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue93.v' -> `./test-suite/issues/issue93.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue346.v' -> `./test-suite/issues/issue346.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue71.v' -> `./test-suite/issues/issue71.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue74.v' -> `./test-suite/issues/issue74.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue228.v' -> `./test-suite/issues/issue228.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue114.v' -> `./test-suite/issues/issue114.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue297.v' -> `./test-suite/issues/issue297.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue240.v' -> `./test-suite/issues/issue240.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue77.v' -> `./test-suite/issues/issue77.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue107_2.v' -> `./test-suite/issues/issue107_2.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue7_extr.v' -> `./test-suite/issues/issue7_extr.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue43.v' -> `./test-suite/issues/issue43.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue81.v' -> `./test-suite/issues/issue81.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue338.v' -> `./test-suite/issues/issue338.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue82.v' -> `./test-suite/issues/issue82.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue73.v' -> `./test-suite/issues/issue73.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue273.v' -> `./test-suite/issues/issue273.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue191.v' -> `./test-suite/issues/issue191.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue120.v' -> `./test-suite/issues/issue120.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue212.v' -> `./test-suite/issues/issue212.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue104.v' -> `./test-suite/issues/issue104.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue_mutual.v' -> `./test-suite/issues/issue_mutual.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue83.v' -> `./test-suite/issues/issue83.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue107.v' -> `./test-suite/issues/issue107.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue117.v' -> `./test-suite/issues/issue117.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue306.v' -> `./test-suite/issues/issue306.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue124.v' -> `./test-suite/issues/issue124.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue99.v' -> `./test-suite/issues/issue99.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue258.v' -> `./test-suite/issues/issue258.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue349.v' -> `./test-suite/issues/issue349.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue176.v' -> `./test-suite/issues/issue176.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue13.v' -> `./test-suite/issues/issue13.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue100.v' -> `./test-suite/issues/issue100.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue143.v' -> `./test-suite/issues/issue143.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue328.v' -> `./test-suite/issues/issue328.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue129.v' -> `./test-suite/issues/issue129.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue193.v' -> `./test-suite/issues/issue193.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue24.v' -> `./test-suite/issues/issue24.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue61.v' -> `./test-suite/issues/issue61.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue272.v' -> `./test-suite/issues/issue272.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue91.v' -> `./test-suite/issues/issue91.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue79.v' -> `./test-suite/issues/issue79.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue286.v' -> `./test-suite/issues/issue286.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue8.v' -> `./test-suite/issues/issue8.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/test-suite/issues/issue190.v' -> `./test-suite/issues/issue190.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/mutualwfrec.v' -> `./examples/mutualwfrec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/function_iter_style.v' -> `./examples/function_iter_style.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/graph_complete.v' -> `./examples/graph_complete.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/string_matching.v' -> `./examples/string_matching.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/nested_mut_rec.v' -> `./examples/nested_mut_rec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/Fin.v' -> `./examples/Fin.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/definterp_simple.v' -> `./examples/definterp_simple.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/_HoTTProject' -> `./examples/_HoTTProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/definterp_scope.v' -> `./examples/definterp_scope.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/definterp.v' -> `./examples/definterp.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/ordinals.v' -> `./examples/ordinals.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/views.v' -> `./examples/views.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/polynomials.v' -> `./examples/polynomials.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/Makefile.local' -> `./examples/Makefile.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/Basics.v' -> `./examples/Basics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/bove_capretta.v' -> `./examples/bove_capretta.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/nm.v' -> `./examples/nm.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/POPLMark1a.v' -> `./examples/POPLMark1a.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/_CoqProject' -> `./examples/_CoqProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/general_recursion.v' -> `./examples/general_recursion.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/MoreDep.v' -> `./examples/MoreDep.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/HoTT_light.v' -> `./examples/HoTT_light.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/quicksort.v' -> `./examples/quicksort.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/ho_finite_branching.v' -> `./examples/ho_finite_branching.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/RoseTree.v' -> `./examples/RoseTree.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/wfrec.v' -> `./examples/wfrec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/AlmostFull.v' -> `./examples/AlmostFull.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/accumulator.v' -> `./examples/accumulator.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/misc.v' -> `./examples/misc.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/STLC.v' -> `./examples/STLC.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/NoConfusion_UIP.v' -> `./theories/NoConfusion_UIP.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Signature.v' -> `./theories/Signature.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/dune' -> `./theories/dune'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Equations.v' -> `./theories/Equations.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/NoCycle.v' -> `./theories/NoCycle.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/CoreTactics.v' -> `./theories/CoreTactics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Init.v' -> `./theories/Init.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Telescopes.v' -> `./theories/HoTT/Telescopes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/All.v' -> `./theories/HoTT/All.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/EqDec.v' -> `./theories/HoTT/EqDec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Loader.v' -> `./theories/HoTT/Loader.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/NoConfusion.v' -> `./theories/HoTT/NoConfusion.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Relation.v' -> `./theories/HoTT/Relation.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/EqDecInstances.v' -> `./theories/HoTT/EqDecInstances.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Subterm.v' -> `./theories/HoTT/Subterm.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/FunctionalInduction.v' -> `./theories/HoTT/FunctionalInduction.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/DepElim.v' -> `./theories/HoTT/DepElim.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Relation_Properties.v' -> `./theories/HoTT/Relation_Properties.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Logic.v' -> `./theories/HoTT/Logic.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Constants.v' -> `./theories/HoTT/Constants.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Classes.v' -> `./theories/HoTT/Classes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/Tactics.v' -> `./theories/HoTT/Tactics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/WellFoundedInstances.v' -> `./theories/HoTT/WellFoundedInstances.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/HoTT/WellFounded.v' -> `./theories/HoTT/WellFounded.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Telescopes.v' -> `./theories/Type/Telescopes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/All.v' -> `./theories/Type/All.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/EqDec.v' -> `./theories/Type/EqDec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Loader.v' -> `./theories/Type/Loader.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/NoConfusion.v' -> `./theories/Type/NoConfusion.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Relation.v' -> `./theories/Type/Relation.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/EqDecInstances.v' -> `./theories/Type/EqDecInstances.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Subterm.v' -> `./theories/Type/Subterm.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/FunctionalExtensionality.v' -> `./theories/Type/FunctionalExtensionality.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/FunctionalInduction.v' -> `./theories/Type/FunctionalInduction.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/DepElim.v' -> `./theories/Type/DepElim.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Relation_Properties.v' -> `./theories/Type/Relation_Properties.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Logic.v' -> `./theories/Type/Logic.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Constants.v' -> `./theories/Type/Constants.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Classes.v' -> `./theories/Type/Classes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/Tactics.v' -> `./theories/Type/Tactics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/WellFoundedInstances.v' -> `./theories/Type/WellFoundedInstances.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Type/WellFounded.v' -> `./theories/Type/WellFounded.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Telescopes.v' -> `./theories/Prop/Telescopes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/EqDec.v' -> `./theories/Prop/EqDec.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Loader.v' -> `./theories/Prop/Loader.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/OpaqueEquations.v' -> `./theories/Prop/OpaqueEquations.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/NoConfusion.v' -> `./theories/Prop/NoConfusion.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/EqDecInstances.v' -> `./theories/Prop/EqDecInstances.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Subterm.v' -> `./theories/Prop/Subterm.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/FunctionalInduction.v' -> `./theories/Prop/FunctionalInduction.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/DepElim.v' -> `./theories/Prop/DepElim.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/TransparentEquations.v' -> `./theories/Prop/TransparentEquations.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Logic.v' -> `./theories/Prop/Logic.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Constants.v' -> `./theories/Prop/Constants.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Classes.v' -> `./theories/Prop/Classes.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/theories/Prop/Tactics.v' -> `./theories/Prop/Tactics.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/utf.sty' -> `./doc/utf.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/equations.tex' -> `./doc/equations.tex'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/stlc.tex' -> `./doc/stlc.tex'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/equations.pdf' -> `./doc/equations.pdf'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/equations_intro.v' -> `./doc/equations_intro.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/code.sty' -> `./doc/code.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/myplainnat.bst' -> `./doc/myplainnat.bst'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/manual.tex' -> `./doc/manual.tex'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/Makefile' -> `./doc/Makefile'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/abbrevs.sty' -> `./doc/abbrevs.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/qsymbols.sty' -> `./doc/qsymbols.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/coq.sty' -> `./doc/coq.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/ml.sty' -> `./doc/ml.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/utfmacros.sty' -> `./doc/utfmacros.sty'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/biblio.bib' -> `./doc/biblio.bib'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/doc/lambda.sty' -> `./doc/lambda.sty'
phase `unpack' succeeded after 0.2 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: ./buildHoTT.sh: changing `/usr/bin/env bash' to `/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./configure.sh: changing `/usr/bin/env bash' to `/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./makedoc.sh: changing `/bin/sh' to `/gnu/store/7zp9ifpgm3zj481nk6jg1im13g4mza2g-bash-minimal-5.0.16/bin/sh'
phase `patch-source-shebangs' succeeded after 0.1 seconds
starting phase `configure'
Building Coq version (default)
phase `configure' succeeded after 0.0 seconds
starting phase `patch-generated-file-shebangs'
phase `patch-generated-file-shebangs' succeeded after 0.0 seconds
starting phase `build'
COQDEP VFILES
COQPP src/g_equations.mlg
CAMLDEP src/extra_tactics.mli
CAMLDEP src/noconf.mli
CAMLDEP src/noconf_hom.mli
CAMLDEP src/equations.mli
CAMLDEP src/principles.mli
CAMLDEP src/principles_proofs.mli
CAMLDEP src/covering.mli
CAMLDEP src/splitting.mli
CAMLDEP src/context_map.mli
CAMLDEP src/simplify.mli
CAMLDEP src/syntax.mli
CAMLDEP src/eqdec.mli
CAMLDEP src/depelim.mli
CAMLDEP src/subterm.mli
CAMLDEP src/sigma_types.mli
CAMLDEP src/ederive.mli
CAMLDEP src/equations_common.mli
OCAMLLIBDEP src/equations_plugin.mllib
CAMLDEP src/equations_plugin_mod.ml
CAMLDEP src/extra_tactics.ml
CAMLDEP src/noconf.ml
CAMLDEP src/noconf_hom.ml
CAMLDEP src/equations.ml
CAMLDEP src/principles.ml
CAMLDEP src/principles_proofs.ml
CAMLDEP src/covering.ml
CAMLDEP src/splitting.ml
CAMLDEP src/simplify.ml
CAMLDEP src/context_map.ml
CAMLDEP src/syntax.ml
CAMLDEP src/depelim.ml
CAMLDEP src/eqdec.ml
CAMLDEP src/subterm.ml
*** Warning: in file theories/Init.v, declared ML module cc_plugin has not been found!
*** Warning: in file theories/Init.v, declared ML module extraction_plugin has not been found!
CAMLDEP src/sigma_types.ml
CAMLDEP src/ederive.ml
CAMLDEP src/equations_common.ml
CAMLDEP src/g_equations.ml
CAMLC -c src/equations_common.mli
CAMLC -c src/ederive.mli
CAMLC -c src/subterm.mli
CAMLC -c src/noconf_hom.mli
CAMLC -c src/noconf.mli
CAMLC -c src/extra_tactics.mli
CAMLOPT -c  src/equations_plugin_mod.ml
CAMLOPT -c  src/ederive.ml
CAMLC -c src/syntax.mli
CAMLC -c src/eqdec.mli
CAMLOPT -c  src/equations_common.ml
CAMLC -c src/context_map.mli
CAMLC -c src/depelim.mli
CAMLC -c src/sigma_types.mli
CAMLC -c src/simplify.mli
CAMLC -c src/splitting.mli
CAMLC -c src/covering.mli
CAMLC -c src/principles_proofs.mli
CAMLC -c src/equations.mli
CAMLC -c src/principles.mli
CAMLOPT -c  src/syntax.ml
CAMLOPT -c  src/eqdec.ml
CAMLOPT -c  src/extra_tactics.ml
CAMLOPT -c  src/context_map.ml
CAMLOPT -c  src/sigma_types.ml
CAMLOPT -c  src/simplify.ml
CAMLOPT -c  src/subterm.ml
CAMLOPT -c  src/splitting.ml
CAMLOPT -c  src/covering.ml
CAMLOPT -c  src/depelim.ml
CAMLOPT -c  src/noconf_hom.ml
CAMLOPT -c  src/noconf.ml
CAMLOPT -c  src/principles_proofs.ml
CAMLOPT -c  src/principles.ml
CAMLOPT -c  src/equations.ml
CAMLOPT -c  src/g_equations.ml
File "src/g_equations.mlg", line 278, characters 28-38:
Alert deprecated: Pcoq.Constr.operconstr
Deprecated in 8.13; use 'term' instead
CAMLOPT -a -o src/equations_plugin.cmxa
CAMLOPT -shared -o src/equations_plugin.cmxs
COQC theories/Init.v
COQC theories/Signature.v
COQC theories/Prop/Logic.v
COQC theories/Type/Logic.v
COQC theories/CoreTactics.v
COQC theories/Type/FunctionalExtensionality.v
COQC theories/Type/Relation.v
COQC theories/Prop/Classes.v
COQC theories/Type/Relation_Properties.v
COQC theories/Prop/EqDec.v
COQC theories/Type/WellFounded.v
COQC theories/Prop/DepElim.v
COQC theories/Type/Classes.v
COQC theories/Type/EqDec.v
COQC theories/Prop/Constants.v
COQC theories/Prop/FunctionalInduction.v
COQC theories/Prop/TransparentEquations.v
COQC theories/Prop/OpaqueEquations.v
COQC theories/Prop/Subterm.v
COQC theories/Type/DepElim.v
COQC theories/Prop/Tactics.v
COQC theories/Type/Constants.v
COQC theories/Type/FunctionalInduction.v
COQC theories/Type/Subterm.v
COQC theories/Prop/NoConfusion.v
COQC theories/Type/Tactics.v
COQC theories/Type/EqDecInstances.v
COQC theories/Type/NoConfusion.v
COQC theories/Prop/EqDecInstances.v
COQC theories/Type/Loader.v
COQC theories/Type/WellFoundedInstances.v
COQC theories/Type/Telescopes.v
COQC theories/Prop/Loader.v
COQC theories/Prop/Telescopes.v
COQC theories/Type/All.v
COQC theories/Equations.v
phase `build' succeeded after 13.9 seconds
starting phase `check'
cd test-suite && coq_makefile -f _CoqProject -o Makefile
cd examples && coq_makefile -f _CoqProject -o Makefile
make[1]: Nothing to be done for 'real-all'.
cd test-suite && make
make[1]: Entering directory '/tmp/guix-build-coq-equations-1.2.4.drv-0/source/test-suite'
COQDEP VFILES
COQC fin.v
COQC notations.v
COQC BasicsDec.v
COQC rec.v
COQC f91.v
COQC Noconfinv.v
COQC zoe.v
COQC gcd.v
COQC DataStruct.v
COQC daaa.v
COQC nestedobls.v
COQC rose.v
COQC scope.v
COQC depelim.v
COQC issues/issue7.v
COQC issues/issue8.v
COQC issues/issue13.v
COQC issues/issue24.v
COQC issues/issue25.v
COQC issues/issue63.v
Closed under the global context
COQC issues/issue66.v
Closed under the global context
COQC issues/issue70.v
COQC issues/issue74.v
     = 6
     : nat
COQC issues/issue75.v
COQC issues/issue77.v
COQC issues/issue79.v
COQC issues/issue81.v
COQC issues/issue83.v
COQC issues/issue82.v
COQC issues/issue84.v
COQC issues/issue85.v
COQC issues/issue91.v
COQC issues/issue95_1.v
COQC issues/issue96.v
COQC issues/issue98.v
COQC issues/issue100.v
COQC issues/issue104.v
COQC issues/issue105.v
COQC issues/issue106.v
COQC issues/issue107.v
COQC issues/issue107_2.v
COQC issues/issue112.v
COQC issues/issue113.v
COQC issues/issue114.v
COQC issues/issue117.v
COQC issues/issue120.v
COQC issues/issue124.v
COQC issues/issue129.v
COQC issues/issue143.v
COQC issues/issue172.v
COQC issues/issue190.v
COQC issues/issue191.v
COQC issues/issue193.v
COQC issues/issue228.v
COQC issues/issue246.v
COQC issues/issue249.v
COQC issues/issue258.v
COQC issues/issue286.v
File "./issues/issue193.v", line 4, characters 0-74:
Warning: h_type_obligations_obligation_1 cannot be used as a hint.
COQC issues/issue297.v
File "./issues/issue193.v", line 16, characters 0-59:
Warning: h_prop_obligations_obligation_1 cannot be used as a hint.
Closed under the global context
COQC issues/issue306.v
COQC issues/issue338.v
COQC issues/issue346.v
Program obligation tactic is Tactics.program_simplify;
                              CoreTactics.equations_simpl;
                              try Tactics.program_solve_wf (globally defined)
COQC issues/issue349.v
COQC eqdec_error.v
COQC noconf_simplify.v
COQC le.v
COQC LogicType.v
COQC mfix.v
COQC mutrec.v
NoConfusionPackage_X : NoConfusionPackage (sigma (fun x : Type => X x))
     : NoConfusionPackage (sigma (fun x : Type => X x))
COQC nestedrec.v
COQC nestedrec2.v
NoConfusion.NoConfusionPackage_list decl : NoConfusionPackage ctx
     : NoConfusionPackage ctx
COQC nestfixnorec.v
COQC agda_1408.v
COQC agda_1775.v
COQC tabareau_vec.v
COQC yves.v
COQC local_where.v
COQC cfold.v
COQC nestedwhererec.v
COQC Below.v
COQC divmod.v
COQC fle_trans.v
COQC interval.v
COQC letred.v
COQC nocycle_def.v
COQC nolam.v
COQC issues/issue95_2.v
COQC nocycle.v
Closed under the global context
Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
    x = eq_rect p Q x p h
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y
Closed under the global context
Closed under the global context
Finished transaction in 2.696 secs (2.651u,0.004s) (successful)
Finished transaction in 2.147 secs (2.096u,0.s) (successful)
Closed under the global context
Closed under the global context
COQC Basics.v
COQC wfnocycle.v
COQC innacs.v
(λ x y : tree,
   apply_noCycle_left x (node y (node y x))
     (clos_trans_stepr tree tree_direct_subterm x 
        (node y x) (node y (node y x)) (tree_direct_subterm_1_1 y (node y x))
        (t_step tree tree_direct_subterm x (node y x)
           (tree_direct_subterm_1_1 y x))))
Finished transaction in 11.438 secs (11.369u,0.012s) (successful)
Closed under the global context
Closed under the global context
make[1]: Leaving directory '/tmp/guix-build-coq-equations-1.2.4.drv-0/source/test-suite'
phase `check' succeeded after 30.5 seconds
starting phase `install'
INSTALL theories/Init.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.vo /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.v /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.glob /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL src/g_equations.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxs /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxa /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/g_equations.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmx /gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
make[1]: Entering directory '/tmp/guix-build-coq-equations-1.2.4.drv-0/source'
make[1]: Leaving directory '/tmp/guix-build-coq-equations-1.2.4.drv-0/source'
phase `install' succeeded after 2.4 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/lib" with "strip" and flags ("--strip-debug" "--enable-deterministic-archives")
phase `strip' succeeded after 0.1 seconds
starting phase `validate-runpath'
validating RUNPATH of 1 binaries in "/gnu/store/6mh9wj2z38q3yb2iaih3ab2m7a0mj719-coq-equations-1.2.4/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 1 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