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/ljvlp2gxx1l49cdw5mh1ydl7336509xy-ocaml-4.11.1/bin:/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/bin:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/bin:/gnu/store/i29bx7l0qpjnypwii4cyayz5fail590d-ocaml-zarith-1.12/bin:/gnu/store/gww59gv5qxbfijg3vk5y182im7923s06-tar-1.32/bin:/gnu/store/2ayciqwxddkzq183dac82ijljc14j4zj-gzip-1.10/bin:/gnu/store/n1jk0w2wa4vpwmixaqn2y3la1l2sizzi-bzip2-1.0.8/bin:/gnu/store/7p36raqgk6vn47bflxc9bsclqiib3phi-xz-5.2.4/bin:/gnu/store/lpkf3ydcdvxn8gcrzaq9cp3ri05h8qhs-file-5.38/bin:/gnu/store/6gqaw09zqw8w0vcax6simlq71bq7l5r0-diffutils-3.7/bin:/gnu/store/qw20chpgkgbcqmzhs60c8hjl1hmblyc8-patch-2.7.6/bin:/gnu/store/b5y5scfmh2d8kxcpl9p84294z2198cgf-findutils-4.7.0/bin:/gnu/store/9iwlsj7d6ffqhshy8qshf7p4fqwfwrvn-gawk-5.0.1/bin:/gnu/store/q1nfjb24vqjs1cgi8mlnskw34h16y09r-sed-4.8/bin:/gnu/store/4qr6mcvsxyzknxa7x1wny8x30f5i0r3n-grep-3.4/bin:/gnu/store/2v61vg0bizgrhybkqbrki2k7kr094waz-coreutils-8.32/bin:/gnu/store/b7jbh7kzzig0bxfswdj8nfj9bkljyyya-make-4.3/bin:/gnu/store/v1g7f3p4f0851mywrla8qmr9hb8jgfjr-bash-minimal-5.0.16/bin:/gnu/store/dyqxnydqk1810afjfbqzfvh0n83xyl62-ld-wrapper-0/bin:/gnu/store/50lyzn9bz6x4da66648kry29wn8afird-binutils-2.34/bin:/gnu/store/afpgzln8860m6yfhxy6i8n9rywbp85cy-gcc-7.5.0/bin:/gnu/store/z4li262il798hbl0l1h1k3a5g7r6bffa-glibc-2.31/bin:/gnu/store/z4li262il798hbl0l1h1k3a5g7r6bffa-glibc-2.31/sbin'
environment variable `OCAMLPATH' set to `/gnu/store/ljvlp2gxx1l49cdw5mh1ydl7336509xy-ocaml-4.11.1/lib/ocaml:/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/lib/ocaml:/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/lib/ocaml/site-lib:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/lib/ocaml:/gnu/store/i29bx7l0qpjnypwii4cyayz5fail590d-ocaml-zarith-1.12/lib/ocaml:/gnu/store/i29bx7l0qpjnypwii4cyayz5fail590d-ocaml-zarith-1.12/lib/ocaml/site-lib'
environment variable `CAML_LD_LIBRARY_PATH' set to `/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/lib/ocaml/site-lib/stublibs:/gnu/store/i29bx7l0qpjnypwii4cyayz5fail590d-ocaml-zarith-1.12/lib/ocaml/site-lib/stublibs'
environment variable `COQPATH' unset
environment variable `COQLIB' set to `/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/lib/ocaml/site-lib/coq'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/n1jk0w2wa4vpwmixaqn2y3la1l2sizzi-bzip2-1.0.8/include:/gnu/store/7p36raqgk6vn47bflxc9bsclqiib3phi-xz-5.2.4/include:/gnu/store/lpkf3ydcdvxn8gcrzaq9cp3ri05h8qhs-file-5.38/include:/gnu/store/9iwlsj7d6ffqhshy8qshf7p4fqwfwrvn-gawk-5.0.1/include:/gnu/store/b7jbh7kzzig0bxfswdj8nfj9bkljyyya-make-4.3/include:/gnu/store/50lyzn9bz6x4da66648kry29wn8afird-binutils-2.34/include:/gnu/store/afpgzln8860m6yfhxy6i8n9rywbp85cy-gcc-7.5.0/include:/gnu/store/z4li262il798hbl0l1h1k3a5g7r6bffa-glibc-2.31/include:/gnu/store/hk7l42fwxmnrnlhyiixvaqf1i1crcckp-linux-libre-headers-5.4.20/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/n1jk0w2wa4vpwmixaqn2y3la1l2sizzi-bzip2-1.0.8/include:/gnu/store/7p36raqgk6vn47bflxc9bsclqiib3phi-xz-5.2.4/include:/gnu/store/lpkf3ydcdvxn8gcrzaq9cp3ri05h8qhs-file-5.38/include:/gnu/store/9iwlsj7d6ffqhshy8qshf7p4fqwfwrvn-gawk-5.0.1/include:/gnu/store/b7jbh7kzzig0bxfswdj8nfj9bkljyyya-make-4.3/include:/gnu/store/50lyzn9bz6x4da66648kry29wn8afird-binutils-2.34/include:/gnu/store/afpgzln8860m6yfhxy6i8n9rywbp85cy-gcc-7.5.0/include/c++:/gnu/store/afpgzln8860m6yfhxy6i8n9rywbp85cy-gcc-7.5.0/include:/gnu/store/z4li262il798hbl0l1h1k3a5g7r6bffa-glibc-2.31/include:/gnu/store/hk7l42fwxmnrnlhyiixvaqf1i1crcckp-linux-libre-headers-5.4.20/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/ljvlp2gxx1l49cdw5mh1ydl7336509xy-ocaml-4.11.1/lib:/gnu/store/hbav4p8v5jq040pn8ylig7l070z2244r-coq-8.13.2/lib:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/lib:/gnu/store/i29bx7l0qpjnypwii4cyayz5fail590d-ocaml-zarith-1.12/lib:/gnu/store/n1jk0w2wa4vpwmixaqn2y3la1l2sizzi-bzip2-1.0.8/lib:/gnu/store/7p36raqgk6vn47bflxc9bsclqiib3phi-xz-5.2.4/lib:/gnu/store/lpkf3ydcdvxn8gcrzaq9cp3ri05h8qhs-file-5.38/lib:/gnu/store/9iwlsj7d6ffqhshy8qshf7p4fqwfwrvn-gawk-5.0.1/lib:/gnu/store/50lyzn9bz6x4da66648kry29wn8afird-binutils-2.34/lib:/gnu/store/z4li262il798hbl0l1h1k3a5g7r6bffa-glibc-2.31/lib:/gnu/store/rzk3v28mhi4m7sh0qippp9a5rzy03rkg-glibc-2.31-static/lib:/gnu/store/x6i3vfg4gaqd42cqb6mzk52v4lds1467-glibc-utf8-locales-2.31/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/x6i3vfg4gaqd42cqb6mzk52v4lds1467-glibc-utf8-locales-2.31/lib/locale'
phase `set-paths' succeeded after 0.0 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/buildHoTT.sh' -> `./buildHoTT.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.coq.local' -> `./Makefile.coq.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/equations.opam' -> `./equations.opam'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/_HoTTProject' -> `./_HoTTProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/configure.sh' -> `./configure.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/dune-project' -> `./dune-project'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/README.dev' -> `./README.dev'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Gemfile' -> `./Gemfile'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/siteexamples.sh' -> `./siteexamples.sh'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/.travis.yml' -> `./.travis.yml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.HoTT.local' -> `./Makefile.HoTT.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/TODO' -> `./TODO'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/README.md' -> `./README.md'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile.local' -> `./Makefile.local'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/Makefile' -> `./Makefile'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/makedoc.sh' -> `./makedoc.sh'
`/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/telescopes.v' -> `./test-suite/telescopes.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/DataStruct.v' -> `./test-suite/DataStruct.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/noconf_noK_fin.v' -> `./test-suite/noconf_noK_fin.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/rec.v' -> `./test-suite/rec.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/daaa.v' -> `./test-suite/daaa.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/Basics.v' -> `./test-suite/Basics.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/nestedwfrec.v' -> `./test-suite/nestedwfrec.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/agda_1775.v' -> `./test-suite/agda_1775.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/Noconfinv.v' -> `./test-suite/Noconfinv.v'
`/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/eqdec_error.v' -> `./test-suite/eqdec_error.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/interval.v' -> `./test-suite/interval.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/gcd.v' -> `./test-suite/gcd.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/LogicType.v' -> `./test-suite/LogicType.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/f91.v' -> `./test-suite/f91.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/nocycle_def.v' -> `./test-suite/nocycle_def.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/square_elim.v' -> `./test-suite/square_elim.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/noconf_noK.v' -> `./test-suite/noconf_noK.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/mfix.v' -> `./test-suite/mfix.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/letred.v' -> `./test-suite/letred.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/pattern_lambdas.v' -> `./test-suite/pattern_lambdas.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/fin.v' -> `./test-suite/fin.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/nestedobls.v' -> `./test-suite/nestedobls.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/tabareau_vec.v' -> `./test-suite/tabareau_vec.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/BasicsHoTT.v' -> `./test-suite/BasicsHoTT.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/noconf_hom.v' -> `./test-suite/noconf_hom.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/BasicsDec.v' -> `./test-suite/BasicsDec.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/terms.v' -> `./test-suite/terms.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/telescopes_nonempty.v' -> `./test-suite/telescopes_nonempty.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/depelim.v' -> `./test-suite/depelim.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/issue66.v' -> `./test-suite/issues/issue66.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/issue74.v' -> `./test-suite/issues/issue74.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/issue200.v' -> `./test-suite/issues/issue200.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/issue7.v' -> `./test-suite/issues/issue7.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/test-suite/issues/issue212.v' -> `./test-suite/issues/issue212.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/issue172.v' -> `./test-suite/issues/issue172.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/issue176.v' -> `./test-suite/issues/issue176.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/issue240.v' -> `./test-suite/issues/issue240.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/issue83.v' -> `./test-suite/issues/issue83.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/issue61.v' -> `./test-suite/issues/issue61.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/issue116.v' -> `./test-suite/issues/issue116.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/issue81.v' -> `./test-suite/issues/issue81.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/issue113.v' -> `./test-suite/issues/issue113.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/issue84.v' -> `./test-suite/issues/issue84.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/issue129.v' -> `./test-suite/issues/issue129.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/issue85.v' -> `./test-suite/issues/issue85.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/issue297.v' -> `./test-suite/issues/issue297.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/issue71.v' -> `./test-suite/issues/issue71.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/issue93.v' -> `./test-suite/issues/issue93.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/issue346.v' -> `./test-suite/issues/issue346.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/issue114.v' -> `./test-suite/issues/issue114.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/issue124.v' -> `./test-suite/issues/issue124.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/issue252.v' -> `./test-suite/issues/issue252.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/issue96.v' -> `./test-suite/issues/issue96.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/issue7_extr.v' -> `./test-suite/issues/issue7_extr.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/issue98.v' -> `./test-suite/issues/issue98.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/issue107.v' -> `./test-suite/issues/issue107.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/issue107_2.v' -> `./test-suite/issues/issue107_2.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/issue105.v' -> `./test-suite/issues/issue105.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/issue328.v' -> `./test-suite/issues/issue328.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/issue77.v' -> `./test-suite/issues/issue77.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/issue43.v' -> `./test-suite/issues/issue43.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/issue8.v' -> `./test-suite/issues/issue8.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/issue249.v' -> `./test-suite/issues/issue249.v'
`/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/NoConfusion_UIP.v' -> `./theories/NoConfusion_UIP.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/CoreTactics.v' -> `./theories/CoreTactics.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/NoCycle.v' -> `./theories/NoCycle.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/NoConfusion.v' -> `./theories/HoTT/NoConfusion.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/HoTT/Telescopes.v' -> `./theories/HoTT/Telescopes.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/WellFoundedInstances.v' -> `./theories/HoTT/WellFoundedInstances.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/Loader.v' -> `./theories/HoTT/Loader.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/Logic.v' -> `./theories/HoTT/Logic.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/EqDecInstances.v' -> `./theories/HoTT/EqDecInstances.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.v' -> `./theories/HoTT/Relation.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/Relation_Properties.v' -> `./theories/HoTT/Relation_Properties.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/Type/EqDec.v' -> `./theories/Type/EqDec.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/WellFounded.v' -> `./theories/Type/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/Classes.v' -> `./theories/Type/Classes.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/Tactics.v' -> `./theories/Type/Tactics.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/Subterm.v' -> `./theories/Type/Subterm.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/All.v' -> `./theories/Type/All.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/DepElim.v' -> `./theories/Type/DepElim.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/Constants.v' -> `./theories/Type/Constants.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/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/Prop/EqDec.v' -> `./theories/Prop/EqDec.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/Telescopes.v' -> `./theories/Prop/Telescopes.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/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/theories/Prop/Loader.v' -> `./theories/Prop/Loader.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/Logic.v' -> `./theories/Prop/Logic.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/EqDecInstances.v' -> `./theories/Prop/EqDecInstances.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/Constants.v' -> `./theories/Prop/Constants.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/examples/definterp.v' -> `./examples/definterp.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/general_recursion.v' -> `./examples/general_recursion.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/function_iter_style.v' -> `./examples/function_iter_style.v'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/examples/_HoTTProject' -> `./examples/_HoTTProject'
`/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/RoseTree.v' -> `./examples/RoseTree.v'
`/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/nm.v' -> `./examples/nm.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/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/mutualwfrec.v' -> `./examples/mutualwfrec.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/quicksort.v' -> `./examples/quicksort.v'
`/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/_CoqProject' -> `./examples/_CoqProject'
`/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/MoreDep.v' -> `./examples/MoreDep.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/string_matching.v' -> `./examples/string_matching.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/graph_complete.v' -> `./examples/graph_complete.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/examples/definterp_simple.v' -> `./examples/definterp_simple.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/POPLMark1a.v' -> `./examples/POPLMark1a.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/nested_mut_rec.v' -> `./examples/nested_mut_rec.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/qsymbols.sty' -> `./doc/qsymbols.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/equations.tex' -> `./doc/equations.tex'
`/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/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/myplainnat.bst' -> `./doc/myplainnat.bst'
`/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/Makefile' -> `./doc/Makefile'
`/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/equations.pdf' -> `./doc/equations.pdf'
`/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/lambda.sty' -> `./doc/lambda.sty'
`/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/.github/workflows/build.yml' -> `./.github/workflows/build.yml'
`/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/ederive.mli' -> `./src/ederive.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/equations.ml' -> `./src/equations.ml'
`/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/eqdec.mli' -> `./src/eqdec.mli'
`/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/simplify.ml' -> `./src/simplify.ml'
`/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/sigma_types.mli' -> `./src/sigma_types.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/principles_proofs.mli' -> `./src/principles_proofs.mli'
`/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/equations_common.mli' -> `./src/equations_common.mli'
`/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/subterm.ml' -> `./src/subterm.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/eqdec.ml' -> `./src/eqdec.ml'
`/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/depelim.mli' -> `./src/depelim.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/extra_tactics.ml' -> `./src/extra_tactics.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/covering.ml' -> `./src/covering.ml'
`/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/dune' -> `./src/dune'
`/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/ederive.ml' -> `./src/ederive.ml'
`/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/principles_proofs.ml' -> `./src/principles_proofs.ml'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/src/depelim.ml' -> `./src/depelim.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/splitting.mli' -> `./src/splitting.mli'
`/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/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/simplify.mli' -> `./src/simplify.mli'
`/gnu/store/rmvwcmk4xmcifgrhm60mhh7ivq06hc7i-coq-equations-1.2.4-checkout/dev/include' -> `./dev/include'
phase `unpack' succeeded after 0.0 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/v1g7f3p4f0851mywrla8qmr9hb8jgfjr-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./configure.sh: changing `/usr/bin/env bash' to `/gnu/store/v1g7f3p4f0851mywrla8qmr9hb8jgfjr-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./makedoc.sh: changing `/bin/sh' to `/gnu/store/v1g7f3p4f0851mywrla8qmr9hb8jgfjr-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_hom.mli
CAMLDEP src/noconf.mli
CAMLDEP src/equations.mli
CAMLDEP src/principles.mli
CAMLDEP src/principles_proofs.mli
*** 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/covering.mli
CAMLDEP src/splitting.mli
CAMLDEP src/simplify.mli
CAMLDEP src/context_map.mli
CAMLDEP src/syntax.mli
CAMLDEP src/depelim.mli
CAMLDEP src/eqdec.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_proofs.ml
CAMLDEP src/principles.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
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
CAMLOPT -c  src/equations_common.ml
CAMLC -c src/syntax.mli
CAMLC -c src/eqdec.mli
CAMLC -c src/context_map.mli
CAMLC -c src/depelim.mli
CAMLC -c src/simplify.mli
CAMLC -c src/sigma_types.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/extra_tactics.ml
CAMLOPT -c  src/eqdec.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/FunctionalInduction.v
COQC theories/Type/Constants.v
COQC theories/Prop/NoConfusion.v
COQC theories/Type/Subterm.v
COQC theories/Type/Tactics.v
COQC theories/Type/NoConfusion.v
COQC theories/Type/EqDecInstances.v
COQC theories/Prop/EqDecInstances.v
COQC theories/Type/Loader.v
COQC theories/Type/Telescopes.v
COQC theories/Type/WellFoundedInstances.v
COQC theories/Prop/Loader.v
COQC theories/Prop/Telescopes.v
COQC theories/Type/All.v
COQC theories/Equations.v
phase `build' succeeded after 12.4 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
Closed under the global context
Closed under the global context
COQC nestedobls.v
     = 6
     : nat
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
Closed under the global context
COQC issues/issue25.v
COQC issues/issue63.v
COQC issues/issue66.v
COQC issues/issue70.v
COQC issues/issue74.v
COQC issues/issue75.v
COQC issues/issue77.v
Closed under the global context
COQC issues/issue79.v
COQC issues/issue81.v
COQC issues/issue82.v
COQC issues/issue83.v
COQC issues/issue84.v
COQC issues/issue85.v
Program obligation tactic is Tactics.program_simplify;
                              CoreTactics.equations_simpl;
                              try Tactics.program_solve_wf (globally defined)
COQC issues/issue91.v
COQC issues/issue95_1.v
COQC issues/issue96.v
COQC issues/issue98.v
COQC issues/issue100.v
Finished transaction in 2.164 secs (1.684u,0.003s) (successful)
Finished transaction in 3.496 secs (2.477u,0.013s) (successful)
COQC issues/issue104.v
COQC issues/issue105.v
COQC issues/issue106.v
COQC issues/issue107.v
Closed under the global context
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
File "./issues/issue193.v", line 4, characters 0-74:
Warning: h_type_obligations_obligation_1 cannot be used as a hint.
File "./issues/issue193.v", line 16, characters 0-59:
Warning: h_prop_obligations_obligation_1 cannot be used as a hint.
COQC issues/issue258.v
COQC issues/issue286.v
COQC issues/issue297.v
COQC issues/issue306.v
COQC issues/issue338.v
COQC issues/issue346.v
COQC issues/issue349.v
COQC eqdec_error.v
COQC noconf_simplify.v
COQC le.v
NoConfusionPackage_X : NoConfusionPackage (sigma (fun x : Type => X x))
     : NoConfusionPackage (sigma (fun x : Type => X x))
COQC LogicType.v
COQC innacs.v
NoConfusion.NoConfusionPackage_list decl : NoConfusionPackage ctx
     : NoConfusionPackage ctx
COQC mfix.v
COQC mutrec.v
COQC nestedrec.v
COQC nestedrec2.v
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
Closed under the global context
COQC wfnocycle.v
COQC divmod.v
COQC fle_trans.v
COQC interval.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 13.856 secs (11.159u,0.044s) (successful)
Closed under the global context
COQC letred.v
COQC nocycle_def.v
COQC nolam.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
COQC Basics.v
COQC issues/issue95_2.v
COQC nocycle.v
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 38.0 seconds
starting phase `install'
INSTALL theories/Init.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.vo /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.v /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.glob /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations//Type
INSTALL src/g_equations.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxs /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxa /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/g_equations.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-coq-equations-1.2.4/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmx /gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-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.1 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/y663lqk6cffl37zxzc8nxzr8134p4mbl-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/y663lqk6cffl37zxzc8nxzr8134p4mbl-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