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/v4fz97i6wvazlk0k3x7ad68ankzpwl4l-ocaml-4.11.1/bin:/gnu/store/cmz4mz44spanlws98b8hsgic05c37ayp-coq-8.11.2/bin:/gnu/store/4h2prk2nn3ji4i9rl5i3xnbwxc48619r-camlp5-7.13/bin:/gnu/store/ggfdxvdgbrjvg2cx3mm7yv5j1y433b01-tar-1.32/bin:/gnu/store/ink6zpk9adb2k2w6a0qif3d45vazl7dv-gzip-1.10/bin:/gnu/store/n8dfjyw11airbnfzz192p9bdbgf31kvj-bzip2-1.0.8/bin:/gnu/store/ggq21is2vyq1jkkqrs90brmwayc4rnmy-xz-5.2.4/bin:/gnu/store/qlxznrl2zzivcln9zgyzw2zshqkjirfs-file-5.38/bin:/gnu/store/yl67anl7279qzrd3kxzj97541jzr2k3d-diffutils-3.7/bin:/gnu/store/w5n1p8kj9zn4zmjhr0bjbknakxij67w2-patch-2.7.6/bin:/gnu/store/x03dmf3xhi3il3mx383zpl4zic38iz1p-findutils-4.7.0/bin:/gnu/store/j80hcnd9p1hh0yb5j1r0gn4vd329a78n-gawk-5.0.1/bin:/gnu/store/wk5vdnms96n2iqfpqyg9gl5lhg8vdc32-sed-4.8/bin:/gnu/store/f3qp8l7f6kmfrvwnyix35kax2lv7lmnb-grep-3.4/bin:/gnu/store/wiv74mq31s0vppzm99qwnjkd8xa3albw-coreutils-8.32/bin:/gnu/store/j7fqszmnydxix8l35d7l3b7dj44qjrw4-make-4.3/bin:/gnu/store/7sfbiqh21h90bc6zi8br1xh60m6qgdd5-bash-minimal-5.0.16/bin:/gnu/store/5m8wvcahy3dgpyhxlq5aq85zbvh5jqfz-ld-wrapper-0/bin:/gnu/store/5371r5kyj50l6176lg6jbfzgfgb2xh14-binutils-2.34/bin:/gnu/store/ap7hgyv4rjqmhg4a6cb6cypsh3g1f5q4-gcc-7.5.0/bin:/gnu/store/cb88z63hyg1icd2kkahiink2p291mhr2-glibc-2.31/bin:/gnu/store/cb88z63hyg1icd2kkahiink2p291mhr2-glibc-2.31/sbin'
environment variable `OCAMLPATH' set to `/gnu/store/v4fz97i6wvazlk0k3x7ad68ankzpwl4l-ocaml-4.11.1/lib/ocaml:/gnu/store/cmz4mz44spanlws98b8hsgic05c37ayp-coq-8.11.2/lib/ocaml:/gnu/store/cmz4mz44spanlws98b8hsgic05c37ayp-coq-8.11.2/lib/ocaml/site-lib:/gnu/store/4h2prk2nn3ji4i9rl5i3xnbwxc48619r-camlp5-7.13/lib/ocaml'
environment variable `CAML_LD_LIBRARY_PATH' unset
environment variable `COQPATH' set to `/gnu/store/cmz4mz44spanlws98b8hsgic05c37ayp-coq-8.11.2/lib/coq/user-contrib'
environment variable `BASH_LOADABLES_PATH' unset
environment variable `C_INCLUDE_PATH' set to `/gnu/store/n8dfjyw11airbnfzz192p9bdbgf31kvj-bzip2-1.0.8/include:/gnu/store/ggq21is2vyq1jkkqrs90brmwayc4rnmy-xz-5.2.4/include:/gnu/store/qlxznrl2zzivcln9zgyzw2zshqkjirfs-file-5.38/include:/gnu/store/j80hcnd9p1hh0yb5j1r0gn4vd329a78n-gawk-5.0.1/include:/gnu/store/j7fqszmnydxix8l35d7l3b7dj44qjrw4-make-4.3/include:/gnu/store/5371r5kyj50l6176lg6jbfzgfgb2xh14-binutils-2.34/include:/gnu/store/ap7hgyv4rjqmhg4a6cb6cypsh3g1f5q4-gcc-7.5.0/include:/gnu/store/cb88z63hyg1icd2kkahiink2p291mhr2-glibc-2.31/include:/gnu/store/nkpdg3jwllrsh7wbkzgflkcpyjn5wp0q-linux-libre-headers-5.4.20/include'
environment variable `CPLUS_INCLUDE_PATH' set to `/gnu/store/n8dfjyw11airbnfzz192p9bdbgf31kvj-bzip2-1.0.8/include:/gnu/store/ggq21is2vyq1jkkqrs90brmwayc4rnmy-xz-5.2.4/include:/gnu/store/qlxznrl2zzivcln9zgyzw2zshqkjirfs-file-5.38/include:/gnu/store/j80hcnd9p1hh0yb5j1r0gn4vd329a78n-gawk-5.0.1/include:/gnu/store/j7fqszmnydxix8l35d7l3b7dj44qjrw4-make-4.3/include:/gnu/store/5371r5kyj50l6176lg6jbfzgfgb2xh14-binutils-2.34/include:/gnu/store/ap7hgyv4rjqmhg4a6cb6cypsh3g1f5q4-gcc-7.5.0/include/c++:/gnu/store/ap7hgyv4rjqmhg4a6cb6cypsh3g1f5q4-gcc-7.5.0/include:/gnu/store/cb88z63hyg1icd2kkahiink2p291mhr2-glibc-2.31/include:/gnu/store/nkpdg3jwllrsh7wbkzgflkcpyjn5wp0q-linux-libre-headers-5.4.20/include'
environment variable `LIBRARY_PATH' set to `/gnu/store/v4fz97i6wvazlk0k3x7ad68ankzpwl4l-ocaml-4.11.1/lib:/gnu/store/cmz4mz44spanlws98b8hsgic05c37ayp-coq-8.11.2/lib:/gnu/store/4h2prk2nn3ji4i9rl5i3xnbwxc48619r-camlp5-7.13/lib:/gnu/store/n8dfjyw11airbnfzz192p9bdbgf31kvj-bzip2-1.0.8/lib:/gnu/store/ggq21is2vyq1jkkqrs90brmwayc4rnmy-xz-5.2.4/lib:/gnu/store/qlxznrl2zzivcln9zgyzw2zshqkjirfs-file-5.38/lib:/gnu/store/j80hcnd9p1hh0yb5j1r0gn4vd329a78n-gawk-5.0.1/lib:/gnu/store/5371r5kyj50l6176lg6jbfzgfgb2xh14-binutils-2.34/lib:/gnu/store/cb88z63hyg1icd2kkahiink2p291mhr2-glibc-2.31/lib:/gnu/store/z7hanmdmdalqh1v0y7z8ilinfhyfh91d-glibc-2.31-static/lib:/gnu/store/4xjcx6g4i229hzzqpqak6vw9bvqh88gi-glibc-utf8-locales-2.31/lib'
environment variable `GUIX_LOCPATH' set to `/gnu/store/4xjcx6g4i229hzzqpqak6vw9bvqh88gi-glibc-utf8-locales-2.31/lib/locale'
phase `set-paths' succeeded after 0.1 seconds
starting phase `install-locale'
using 'en_US.utf8' locale for category "LC_ALL"
phase `install-locale' succeeded after 0.0 seconds
starting phase `unpack'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/siteexamples.sh' -> `./siteexamples.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/_HoTTProject' -> `./_HoTTProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/README.md' -> `./README.md'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/dune' -> `./dune'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/equations.opam' -> `./equations.opam'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile' -> `./Makefile'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/configure.sh' -> `./configure.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Gemfile' -> `./Gemfile'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/.travis.yml' -> `./.travis.yml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile.local' -> `./Makefile.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/README.dev' -> `./README.dev'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/TODO' -> `./TODO'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/buildHoTT.sh' -> `./buildHoTT.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile.coq.local' -> `./Makefile.coq.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/makedoc.sh' -> `./makedoc.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/dune-project' -> `./dune-project'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile.HoTT.local' -> `./Makefile.HoTT.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/principles_proofs.ml' -> `./src/principles_proofs.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/depelim.mli' -> `./src/depelim.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations_common.mli' -> `./src/equations_common.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/principles_proofs.mli' -> `./src/principles_proofs.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/sigma_types.mli' -> `./src/sigma_types.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations.ml' -> `./src/equations.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/g_equations.mlg' -> `./src/g_equations.mlg'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/splitting.mli' -> `./src/splitting.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations_common.ml' -> `./src/equations_common.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/dune' -> `./src/dune'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/ederive.ml' -> `./src/ederive.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/covering.ml' -> `./src/covering.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/principles.ml' -> `./src/principles.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/simplify.mli' -> `./src/simplify.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/sigma_types.ml' -> `./src/sigma_types.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/noconf.mli' -> `./src/noconf.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/extra_tactics.mli' -> `./src/extra_tactics.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/noconf_hom.ml' -> `./src/noconf_hom.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations_plugin.mllib' -> `./src/equations_plugin.mllib'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/noconf_hom.mli' -> `./src/noconf_hom.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/syntax.mli' -> `./src/syntax.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/ederive.mli' -> `./src/ederive.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/subterm.ml' -> `./src/subterm.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations.mli' -> `./src/equations.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/splitting.ml' -> `./src/splitting.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/extra_tactics.ml' -> `./src/extra_tactics.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/context_map.ml' -> `./src/context_map.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/eqdec.ml' -> `./src/eqdec.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/subterm.mli' -> `./src/subterm.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/syntax.ml' -> `./src/syntax.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/principles.mli' -> `./src/principles.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/noconf.ml' -> `./src/noconf.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/eqdec.mli' -> `./src/eqdec.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/context_map.mli' -> `./src/context_map.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/equations_plugin_mod.ml' -> `./src/equations_plugin_mod.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/simplify.ml' -> `./src/simplify.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/covering.mli' -> `./src/covering.mli'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/src/depelim.ml' -> `./src/depelim.ml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/dev/include' -> `./dev/include'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/noconf_hom.v' -> `./test-suite/noconf_hom.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/f91.v' -> `./test-suite/f91.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/interval.v' -> `./test-suite/interval.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/univpoly.v' -> `./test-suite/univpoly.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/rec.v' -> `./test-suite/rec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/terms.v' -> `./test-suite/terms.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/cfold.v' -> `./test-suite/cfold.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/innacs.v' -> `./test-suite/innacs.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/fle_trans.v' -> `./test-suite/fle_trans.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/square_elim.v' -> `./test-suite/square_elim.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/Noconfinv.v' -> `./test-suite/Noconfinv.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/LogicType.v' -> `./test-suite/LogicType.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/noconf_noK_fin.v' -> `./test-suite/noconf_noK_fin.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/daaa.v' -> `./test-suite/daaa.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/le.v' -> `./test-suite/le.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestfixnorec.v' -> `./test-suite/nestfixnorec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/gcd.v' -> `./test-suite/gcd.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/wfnocycle.v' -> `./test-suite/wfnocycle.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/rose.v' -> `./test-suite/rose.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/agda_1775_full.v' -> `./test-suite/agda_1775_full.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/agda_1408.v' -> `./test-suite/agda_1408.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedwhererec.v' -> `./test-suite/nestedwhererec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedrec.v' -> `./test-suite/nestedrec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/tabareau_vec.v' -> `./test-suite/tabareau_vec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/ack.v' -> `./test-suite/ack.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/scope_noK.v' -> `./test-suite/scope_noK.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/pattern_lambdas.v' -> `./test-suite/pattern_lambdas.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/noconf_simplify.v' -> `./test-suite/noconf_simplify.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/mutrec_enc.v' -> `./test-suite/mutrec_enc.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/mutrec.v' -> `./test-suite/mutrec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/scope.v' -> `./test-suite/scope.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/agda_1775.v' -> `./test-suite/agda_1775.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/letred.v' -> `./test-suite/letred.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/noconf_noK.v' -> `./test-suite/noconf_noK.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/telescopes.v' -> `./test-suite/telescopes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/telescopes_nonempty.v' -> `./test-suite/telescopes_nonempty.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/eqdec_error.v' -> `./test-suite/eqdec_error.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/yves.v' -> `./test-suite/yves.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/Basics.v' -> `./test-suite/Basics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/divmod.v' -> `./test-suite/divmod.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedwhererecwith.v' -> `./test-suite/nestedwhererecwith.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/Noconflet.v' -> `./test-suite/Noconflet.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/DataStruct.v' -> `./test-suite/DataStruct.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/fin.v' -> `./test-suite/fin.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/_CoqProject' -> `./test-suite/_CoqProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/Below.v' -> `./test-suite/Below.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/zoe.v' -> `./test-suite/zoe.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedwfrec.v' -> `./test-suite/nestedwfrec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/depelim.v' -> `./test-suite/depelim.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedrec2.v' -> `./test-suite/nestedrec2.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/BasicsDec.v' -> `./test-suite/BasicsDec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nestedobls.v' -> `./test-suite/nestedobls.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/BasicsHoTT.v' -> `./test-suite/BasicsHoTT.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/mfix.v' -> `./test-suite/mfix.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nocycle.v' -> `./test-suite/nocycle.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/local_where.v' -> `./test-suite/local_where.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/notations.v' -> `./test-suite/notations.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nolam.v' -> `./test-suite/nolam.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/nocycle_def.v' -> `./test-suite/nocycle_def.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue96.v' -> `./test-suite/issues/issue96.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue25.v' -> `./test-suite/issues/issue25.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue172.v' -> `./test-suite/issues/issue172.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue246.v' -> `./test-suite/issues/issue246.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue7.v' -> `./test-suite/issues/issue7.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue66.v' -> `./test-suite/issues/issue66.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue70.v' -> `./test-suite/issues/issue70.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue63.v' -> `./test-suite/issues/issue63.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue116.v' -> `./test-suite/issues/issue116.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue98.v' -> `./test-suite/issues/issue98.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue106.v' -> `./test-suite/issues/issue106.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue112.v' -> `./test-suite/issues/issue112.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue85.v' -> `./test-suite/issues/issue85.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue75.v' -> `./test-suite/issues/issue75.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue113.v' -> `./test-suite/issues/issue113.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue105.v' -> `./test-suite/issues/issue105.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue95_1.v' -> `./test-suite/issues/issue95_1.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue95_2.v' -> `./test-suite/issues/issue95_2.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue249.v' -> `./test-suite/issues/issue249.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue84.v' -> `./test-suite/issues/issue84.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue93.v' -> `./test-suite/issues/issue93.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue71.v' -> `./test-suite/issues/issue71.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue74.v' -> `./test-suite/issues/issue74.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue114.v' -> `./test-suite/issues/issue114.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue297.v' -> `./test-suite/issues/issue297.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue77.v' -> `./test-suite/issues/issue77.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue107_2.v' -> `./test-suite/issues/issue107_2.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue7_extr.v' -> `./test-suite/issues/issue7_extr.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue43.v' -> `./test-suite/issues/issue43.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue81.v' -> `./test-suite/issues/issue81.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue82.v' -> `./test-suite/issues/issue82.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue73.v' -> `./test-suite/issues/issue73.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue273.v' -> `./test-suite/issues/issue273.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue191.v' -> `./test-suite/issues/issue191.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue120.v' -> `./test-suite/issues/issue120.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue104.v' -> `./test-suite/issues/issue104.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue83.v' -> `./test-suite/issues/issue83.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue107.v' -> `./test-suite/issues/issue107.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue117.v' -> `./test-suite/issues/issue117.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue124.v' -> `./test-suite/issues/issue124.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue99.v' -> `./test-suite/issues/issue99.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue258.v' -> `./test-suite/issues/issue258.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue176.v' -> `./test-suite/issues/issue176.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue13.v' -> `./test-suite/issues/issue13.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue100.v' -> `./test-suite/issues/issue100.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue143.v' -> `./test-suite/issues/issue143.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue129.v' -> `./test-suite/issues/issue129.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue193.v' -> `./test-suite/issues/issue193.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue24.v' -> `./test-suite/issues/issue24.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue61.v' -> `./test-suite/issues/issue61.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue91.v' -> `./test-suite/issues/issue91.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue79.v' -> `./test-suite/issues/issue79.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue286.v' -> `./test-suite/issues/issue286.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue8.v' -> `./test-suite/issues/issue8.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/test-suite/issues/issue190.v' -> `./test-suite/issues/issue190.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/mutualwfrec.v' -> `./examples/mutualwfrec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/function_iter_style.v' -> `./examples/function_iter_style.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/graph_complete.v' -> `./examples/graph_complete.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/string_matching.v' -> `./examples/string_matching.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/nested_mut_rec.v' -> `./examples/nested_mut_rec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/Fin.v' -> `./examples/Fin.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/definterp_simple.v' -> `./examples/definterp_simple.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/_HoTTProject' -> `./examples/_HoTTProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/definterp_scope.v' -> `./examples/definterp_scope.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/definterp.v' -> `./examples/definterp.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/ordinals.v' -> `./examples/ordinals.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/views.v' -> `./examples/views.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/polynomials.v' -> `./examples/polynomials.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/Makefile.local' -> `./examples/Makefile.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/Basics.v' -> `./examples/Basics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/bove_capretta.v' -> `./examples/bove_capretta.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/nm.v' -> `./examples/nm.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/POPLMark1a.v' -> `./examples/POPLMark1a.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/_CoqProject' -> `./examples/_CoqProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/general_recursion.v' -> `./examples/general_recursion.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/MoreDep.v' -> `./examples/MoreDep.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/HoTT_light.v' -> `./examples/HoTT_light.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/quicksort.v' -> `./examples/quicksort.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/ho_finite_branching.v' -> `./examples/ho_finite_branching.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/RoseTree.v' -> `./examples/RoseTree.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/wfrec.v' -> `./examples/wfrec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/AlmostFull.v' -> `./examples/AlmostFull.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/accumulator.v' -> `./examples/accumulator.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/misc.v' -> `./examples/misc.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/STLC.v' -> `./examples/STLC.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/NoConfusion_UIP.v' -> `./theories/NoConfusion_UIP.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Signature.v' -> `./theories/Signature.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Equations.v' -> `./theories/Equations.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/NoCycle.v' -> `./theories/NoCycle.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/CoreTactics.v' -> `./theories/CoreTactics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Init.v' -> `./theories/Init.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Telescopes.v' -> `./theories/HoTT/Telescopes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/All.v' -> `./theories/HoTT/All.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/EqDec.v' -> `./theories/HoTT/EqDec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Loader.v' -> `./theories/HoTT/Loader.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/NoConfusion.v' -> `./theories/HoTT/NoConfusion.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Relation.v' -> `./theories/HoTT/Relation.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/EqDecInstances.v' -> `./theories/HoTT/EqDecInstances.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Subterm.v' -> `./theories/HoTT/Subterm.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/FunctionalInduction.v' -> `./theories/HoTT/FunctionalInduction.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/DepElim.v' -> `./theories/HoTT/DepElim.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Relation_Properties.v' -> `./theories/HoTT/Relation_Properties.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Logic.v' -> `./theories/HoTT/Logic.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Constants.v' -> `./theories/HoTT/Constants.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Classes.v' -> `./theories/HoTT/Classes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/Tactics.v' -> `./theories/HoTT/Tactics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/WellFoundedInstances.v' -> `./theories/HoTT/WellFoundedInstances.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/HoTT/WellFounded.v' -> `./theories/HoTT/WellFounded.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Telescopes.v' -> `./theories/Type/Telescopes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/All.v' -> `./theories/Type/All.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/EqDec.v' -> `./theories/Type/EqDec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Loader.v' -> `./theories/Type/Loader.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/NoConfusion.v' -> `./theories/Type/NoConfusion.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Relation.v' -> `./theories/Type/Relation.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/EqDecInstances.v' -> `./theories/Type/EqDecInstances.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Subterm.v' -> `./theories/Type/Subterm.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/FunctionalExtensionality.v' -> `./theories/Type/FunctionalExtensionality.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/FunctionalInduction.v' -> `./theories/Type/FunctionalInduction.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/DepElim.v' -> `./theories/Type/DepElim.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Relation_Properties.v' -> `./theories/Type/Relation_Properties.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Logic.v' -> `./theories/Type/Logic.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Constants.v' -> `./theories/Type/Constants.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Classes.v' -> `./theories/Type/Classes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/Tactics.v' -> `./theories/Type/Tactics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/WellFoundedInstances.v' -> `./theories/Type/WellFoundedInstances.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Type/WellFounded.v' -> `./theories/Type/WellFounded.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Telescopes.v' -> `./theories/Prop/Telescopes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/EqDec.v' -> `./theories/Prop/EqDec.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Loader.v' -> `./theories/Prop/Loader.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/OpaqueEquations.v' -> `./theories/Prop/OpaqueEquations.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/NoConfusion.v' -> `./theories/Prop/NoConfusion.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/EqDecInstances.v' -> `./theories/Prop/EqDecInstances.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Subterm.v' -> `./theories/Prop/Subterm.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/FunctionalInduction.v' -> `./theories/Prop/FunctionalInduction.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/DepElim.v' -> `./theories/Prop/DepElim.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/TransparentEquations.v' -> `./theories/Prop/TransparentEquations.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Logic.v' -> `./theories/Prop/Logic.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Constants.v' -> `./theories/Prop/Constants.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Classes.v' -> `./theories/Prop/Classes.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/theories/Prop/Tactics.v' -> `./theories/Prop/Tactics.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/utf.sty' -> `./doc/utf.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/equations.tex' -> `./doc/equations.tex'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/stlc.tex' -> `./doc/stlc.tex'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/equations.pdf' -> `./doc/equations.pdf'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/equations_intro.v' -> `./doc/equations_intro.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/code.sty' -> `./doc/code.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/myplainnat.bst' -> `./doc/myplainnat.bst'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/manual.tex' -> `./doc/manual.tex'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/Makefile' -> `./doc/Makefile'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/abbrevs.sty' -> `./doc/abbrevs.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/qsymbols.sty' -> `./doc/qsymbols.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/coq.sty' -> `./doc/coq.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/ml.sty' -> `./doc/ml.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/utfmacros.sty' -> `./doc/utfmacros.sty'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/biblio.bib' -> `./doc/biblio.bib'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/lambda.sty' -> `./doc/lambda.sty'
phase `unpack' succeeded after 0.2 seconds
starting phase `bootstrap'
no 'configure.ac' or anything like that, doing nothing
phase `bootstrap' succeeded after 0.0 seconds
starting phase `patch-usr-bin-file'
phase `patch-usr-bin-file' succeeded after 0.0 seconds
starting phase `patch-source-shebangs'
patch-shebang: ./buildHoTT.sh: changing `/usr/bin/env bash' to `/gnu/store/7sfbiqh21h90bc6zi8br1xh60m6qgdd5-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./configure.sh: changing `/usr/bin/env bash' to `/gnu/store/7sfbiqh21h90bc6zi8br1xh60m6qgdd5-bash-minimal-5.0.16/bin/bash'
patch-shebang: ./makedoc.sh: changing `/bin/sh' to `/gnu/store/7sfbiqh21h90bc6zi8br1xh60m6qgdd5-bash-minimal-5.0.16/bin/sh'
phase `patch-source-shebangs' succeeded after 0.0 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
*** 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/extra_tactics.mli
CAMLDEP src/noconf.mli
CAMLDEP src/equations.mli
CAMLDEP src/noconf_hom.mli
CAMLDEP src/principles_proofs.mli
CAMLDEP src/principles.mli
CAMLDEP src/covering.mli
CAMLDEP src/splitting.mli
CAMLDEP src/context_map.mli
CAMLDEP src/simplify.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
CAMLDEP src/noconf.ml
CAMLDEP src/extra_tactics.ml
CAMLDEP src/noconf_hom.ml
CAMLDEP src/equations.ml
CAMLDEP src/equations_plugin_mod.ml
CAMLDEP src/principles.ml
CAMLDEP src/principles_proofs.ml
COQDEP src/equations_plugin.mllib
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
CAMLC -c src/eqdec.mli
CAMLC -c src/syntax.mli
CAMLOPT -c  src/equations_common.ml
CAMLC -c src/context_map.mli
CAMLC -c src/depelim.mli
CAMLC -c src/sigma_types.mli
CAMLC -c src/simplify.mli
CAMLC -c src/splitting.mli
CAMLC -c src/covering.mli
CAMLC -c src/equations.mli
CAMLC -c src/principles_proofs.mli
CAMLC -c src/principles.mli
CAMLOPT -c  src/syntax.ml
CAMLOPT -c  src/eqdec.ml
CAMLOPT -c  src/extra_tactics.ml
CAMLOPT -c  src/context_map.ml
CAMLOPT -c  src/sigma_types.ml
CAMLOPT -c  src/simplify.ml
CAMLOPT -c  src/subterm.ml
CAMLOPT -c  src/splitting.ml
CAMLOPT -c  src/covering.ml
CAMLOPT -c  src/noconf_hom.ml
CAMLOPT -c  src/depelim.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
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/Prop/EqDec.v
COQC theories/Type/Relation_Properties.v
COQC theories/Type/WellFounded.v
COQC theories/Prop/DepElim.v
COQC theories/Type/Classes.v
COQC theories/Prop/Constants.v
COQC theories/Prop/FunctionalInduction.v
COQC theories/Prop/OpaqueEquations.v
COQC theories/Prop/TransparentEquations.v
COQC theories/Type/EqDec.v
COQC theories/Prop/Subterm.v
COQC theories/Type/DepElim.v
COQC theories/Prop/Tactics.v
COQC theories/Type/Constants.v
COQC theories/Type/FunctionalInduction.v
COQC theories/Type/Subterm.v
COQC theories/Prop/NoConfusion.v
COQC theories/Type/Tactics.v
COQC theories/Type/EqDecInstances.v
COQC theories/Type/NoConfusion.v
COQC theories/Prop/EqDecInstances.v
COQC theories/Type/Loader.v
COQC theories/Type/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 23.1 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.3.drv-0/source/test-suite'
COQDEP VFILES
COQC fin.v
COQC notations.v
COQC BasicsDec.v
COQC f91.v
COQC Noconfinv.v
COQC rec.v
COQC gcd.v
COQC zoe.v
COQC daaa.v
COQC DataStruct.v
COQC nestedobls.v
COQC rose.v
COQC scope.v
COQC depelim.v
COQC issues/issue7.v
COQC issues/issue8.v
COQC issues/issue13.v
Closed under the global context
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
     = 6
     : nat
COQC issues/issue79.v
COQC issues/issue81.v
COQC issues/issue82.v
COQC issues/issue83.v
COQC issues/issue84.v
COQC issues/issue85.v
COQC issues/issue91.v
COQC issues/issue95_1.v
COQC issues/issue96.v
COQC issues/issue98.v
Closed under the global context
COQC issues/issue100.v
COQC issues/issue104.v
COQC issues/issue105.v
COQC issues/issue106.v
COQC issues/issue107.v
COQC issues/issue107_2.v
COQC issues/issue112.v
COQC issues/issue113.v
COQC issues/issue114.v
COQC issues/issue117.v
COQC issues/issue120.v
COQC issues/issue124.v
COQC issues/issue129.v
COQC issues/issue143.v
COQC issues/issue172.v
COQC issues/issue190.v
COQC issues/issue191.v
COQC issues/issue193.v
Program obligation tactic is Tactics.program_simplify;
                              CoreTactics.equations_simpl;
                              try Tactics.program_solve_wf (globally defined)
COQC issues/issue246.v
COQC issues/issue249.v
COQC issues/issue258.v
COQC issues/issue286.v
COQC issues/issue297.v
COQC eqdec_error.v
Closed under the global context
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 noconf_simplify.v
COQC le.v
Finished transaction in 3.374 secs (2.534u,0.003s) (successful)
COQC LogicType.v
COQC mfix.v
COQC mutrec.v
COQC nestedrec.v
COQC nestedrec2.v
COQC nestfixnorec.v
COQC agda_1408.v
COQC agda_1775.v
NoConfusion.NoConfusionPackage_list decl : NoConfusionPackage ctx
     : NoConfusionPackage ctx
COQC tabareau_vec.v
COQC yves.v
COQC local_where.v
COQC cfold.v
COQC nestedwhererec.v
Finished transaction in 4.499 secs (4.328u,0.s) (successful)
COQC Below.v
COQC divmod.v
COQC fle_trans.v
COQC interval.v
COQC letred.v
COQC nocycle_def.v
COQC nolam.v
File "./fle_trans.v", line 12, characters 0-17:
Warning: Argument number 0 is a trailing implicit so must be maximal
[set-maximal-deprecated,deprecated]
Closed under the global context
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 issues/issue95_2.v
COQC nocycle.v
Closed under the global context
COQC innacs.v
COQC Basics.v
COQC wfnocycle.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))))
Closed under the global context
Finished transaction in 18.219 secs (15.985u,0.023s) (successful)
Closed under the global context
Closed under the global context
make[1]: Leaving directory '/tmp/guix-build-coq-equations-1.2.3.drv-0/source/test-suite'
phase `check' succeeded after 46.6 seconds
starting phase `install'
INSTALL theories/Init.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.vo /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.v /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.glob /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL src/g_equations.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxs /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxa /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/g_equations.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmx /gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
make[1]: Entering directory '/tmp/guix-build-coq-equations-1.2.3.drv-0/source'
make[1]: Leaving directory '/tmp/guix-build-coq-equations-1.2.3.drv-0/source'
phase `install' succeeded after 3.0 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/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/ff1qa2las6zylxpqqxpirnhnzlaxrr4g-coq-equations-1.2.3/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