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