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/y9gw7sf1fpp5nn16yhay2agddcb72zvj-coq-8.11.2/bin:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/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/y9gw7sf1fpp5nn16yhay2agddcb72zvj-coq-8.11.2/lib/ocaml:/gnu/store/y9gw7sf1fpp5nn16yhay2agddcb72zvj-coq-8.11.2/lib/ocaml/site-lib:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/lib/ocaml'
environment variable `CAML_LD_LIBRARY_PATH' unset
environment variable `COQPATH' set to `/gnu/store/y9gw7sf1fpp5nn16yhay2agddcb72zvj-coq-8.11.2/lib/coq/user-contrib'
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/y9gw7sf1fpp5nn16yhay2agddcb72zvj-coq-8.11.2/lib:/gnu/store/y3s6qna9isaxhnx4k22487wg8ahr7l1n-camlp5-7.13/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/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/.travis.yml' -> `./.travis.yml'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/README.dev' -> `./README.dev'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/makedoc.sh' -> `./makedoc.sh'
`/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/Makefile.coq.local' -> `./Makefile.coq.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile.local' -> `./Makefile.local'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/siteexamples.sh' -> `./siteexamples.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/LICENSE' -> `./LICENSE'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/_CoqProject' -> `./_CoqProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Makefile.HoTT.local' -> `./Makefile.HoTT.local'
`/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/configure.sh' -> `./configure.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/dune-project' -> `./dune-project'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/.gitignore' -> `./.gitignore'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/buildHoTT.sh' -> `./buildHoTT.sh'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/TODO' -> `./TODO'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/_HoTTProject' -> `./_HoTTProject'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/Gemfile' -> `./Gemfile'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/dev/include' -> `./dev/include'
`/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/abbrevs.sty' -> `./doc/abbrevs.sty'
`/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/Makefile' -> `./doc/Makefile'
`/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/myplainnat.bst' -> `./doc/myplainnat.bst'
`/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/equations_intro.v' -> `./doc/equations_intro.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/doc/lambda.sty' -> `./doc/lambda.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/coq.sty' -> `./doc/coq.sty'
`/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/manual.tex' -> `./doc/manual.tex'
`/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/utf.sty' -> `./doc/utf.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/src/syntax.mli' -> `./src/syntax.mli'
`/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/equations_common.ml' -> `./src/equations_common.ml'
`/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/subterm.ml' -> `./src/subterm.ml'
`/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/sigma_types.mli' -> `./src/sigma_types.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/noconf.mli' -> `./src/noconf.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/g_equations.mlg' -> `./src/g_equations.mlg'
`/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/noconf_hom.ml' -> `./src/noconf_hom.ml'
`/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/covering.mli' -> `./src/covering.mli'
`/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/extra_tactics.ml' -> `./src/extra_tactics.ml'
`/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/dune' -> `./src/dune'
`/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/depelim.mli' -> `./src/depelim.mli'
`/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/syntax.ml' -> `./src/syntax.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/ederive.ml' -> `./src/ederive.ml'
`/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/principles.mli' -> `./src/principles.mli'
`/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/equations_common.mli' -> `./src/equations_common.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/src/eqdec.mli' -> `./src/eqdec.mli'
`/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/noconf_hom.mli' -> `./src/noconf_hom.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/splitting.ml' -> `./src/splitting.ml'
`/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/principles.ml' -> `./src/principles.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/theories/CoreTactics.v' -> `./theories/CoreTactics.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/Init.v' -> `./theories/Init.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/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/Type/DepElim.v' -> `./theories/Type/DepElim.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/Classes.v' -> `./theories/Type/Classes.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/Constants.v' -> `./theories/Type/Constants.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/Tactics.v' -> `./theories/Type/Tactics.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/Type/Relation_Properties.v' -> `./theories/Type/Relation_Properties.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/FunctionalExtensionality.v' -> `./theories/Type/FunctionalExtensionality.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/Telescopes.v' -> `./theories/Type/Telescopes.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/NoConfusion.v' -> `./theories/Type/NoConfusion.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/Subterm.v' -> `./theories/Type/Subterm.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/Prop/DepElim.v' -> `./theories/Prop/DepElim.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/EqDecInstances.v' -> `./theories/Prop/EqDecInstances.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/Constants.v' -> `./theories/Prop/Constants.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/Tactics.v' -> `./theories/Prop/Tactics.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/TransparentEquations.v' -> `./theories/Prop/TransparentEquations.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/Logic.v' -> `./theories/Prop/Logic.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/FunctionalInduction.v' -> `./theories/Prop/FunctionalInduction.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/HoTT/DepElim.v' -> `./theories/HoTT/DepElim.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/Classes.v' -> `./theories/HoTT/Classes.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/Constants.v' -> `./theories/HoTT/Constants.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/Tactics.v' -> `./theories/HoTT/Tactics.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/HoTT/Relation_Properties.v' -> `./theories/HoTT/Relation_Properties.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/Relation.v' -> `./theories/HoTT/Relation.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/Logic.v' -> `./theories/HoTT/Logic.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/FunctionalInduction.v' -> `./theories/HoTT/FunctionalInduction.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/WellFoundedInstances.v' -> `./theories/HoTT/WellFoundedInstances.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/interval.v' -> `./test-suite/interval.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/BasicsHoTT.v' -> `./test-suite/BasicsHoTT.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/zoe.v' -> `./test-suite/zoe.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/Below.v' -> `./test-suite/Below.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/BasicsDec.v' -> `./test-suite/BasicsDec.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/nestedwhererecwith.v' -> `./test-suite/nestedwhererecwith.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/nestedwhererec.v' -> `./test-suite/nestedwhererec.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/nestfixnorec.v' -> `./test-suite/nestfixnorec.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/nestedwfrec.v' -> `./test-suite/nestedwfrec.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/mutrec_enc.v' -> `./test-suite/mutrec_enc.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/noconf_hom.v' -> `./test-suite/noconf_hom.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/nestedrec2.v' -> `./test-suite/nestedrec2.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/cfold.v' -> `./test-suite/cfold.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/Noconflet.v' -> `./test-suite/Noconflet.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/_CoqProject' -> `./test-suite/_CoqProject'
`/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/nestedobls.v' -> `./test-suite/nestedobls.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/innacs.v' -> `./test-suite/innacs.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/noconf_noK.v' -> `./test-suite/noconf_noK.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/nocycle.v' -> `./test-suite/nocycle.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/agda_1775.v' -> `./test-suite/agda_1775.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/telescopes.v' -> `./test-suite/telescopes.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/mutrec.v' -> `./test-suite/mutrec.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/daaa.v' -> `./test-suite/daaa.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/divmod.v' -> `./test-suite/divmod.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/DataStruct.v' -> `./test-suite/DataStruct.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/noconf_noK_fin.v' -> `./test-suite/noconf_noK_fin.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/scope_noK.v' -> `./test-suite/scope_noK.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/rose.v' -> `./test-suite/rose.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/LogicType.v' -> `./test-suite/LogicType.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/issues/issue84.v' -> `./test-suite/issues/issue84.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/issue104.v' -> `./test-suite/issues/issue104.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/issue75.v' -> `./test-suite/issues/issue75.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/issue107.v' -> `./test-suite/issues/issue107.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/issue74.v' -> `./test-suite/issues/issue74.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/issue95_1.v' -> `./test-suite/issues/issue95_1.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/issue190.v' -> `./test-suite/issues/issue190.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/issue143.v' -> `./test-suite/issues/issue143.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/issue107_2.v' -> `./test-suite/issues/issue107_2.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/issue91.v' -> `./test-suite/issues/issue91.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/issue120.v' -> `./test-suite/issues/issue120.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/issue172.v' -> `./test-suite/issues/issue172.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/issue105.v' -> `./test-suite/issues/issue105.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/issue70.v' -> `./test-suite/issues/issue70.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/issue7_extr.v' -> `./test-suite/issues/issue7_extr.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/issue193.v' -> `./test-suite/issues/issue193.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/issue77.v' -> `./test-suite/issues/issue77.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/issue176.v' -> `./test-suite/issues/issue176.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/issue73.v' -> `./test-suite/issues/issue73.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/issue98.v' -> `./test-suite/issues/issue98.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/issue8.v' -> `./test-suite/issues/issue8.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/issue273.v' -> `./test-suite/issues/issue273.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/issue114.v' -> `./test-suite/issues/issue114.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/issue249.v' -> `./test-suite/issues/issue249.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/issue71.v' -> `./test-suite/issues/issue71.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/issue43.v' -> `./test-suite/issues/issue43.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/issue95_2.v' -> `./test-suite/issues/issue95_2.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/issue85.v' -> `./test-suite/issues/issue85.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/bove_capretta.v' -> `./examples/bove_capretta.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/definterp_simple.v' -> `./examples/definterp_simple.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/string_matching.v' -> `./examples/string_matching.v'
`/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/Makefile.local' -> `./examples/Makefile.local'
`/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/views.v' -> `./examples/views.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/Fin.v' -> `./examples/Fin.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/polynomials.v' -> `./examples/polynomials.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/_CoqProject' -> `./examples/_CoqProject'
`/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/RoseTree.v' -> `./examples/RoseTree.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/definterp_scope.v' -> `./examples/definterp_scope.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/STLC.v' -> `./examples/STLC.v'
`/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/graph_complete.v' -> `./examples/graph_complete.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/_HoTTProject' -> `./examples/_HoTTProject'
`/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/nested_mut_rec.v' -> `./examples/nested_mut_rec.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/ordinals.v' -> `./examples/ordinals.v'
`/gnu/store/f0gj04gldjs4qba5sjf9ypyg6dkz4018-coq-equations-1.2.3-checkout/examples/accumulator.v' -> `./examples/accumulator.v'
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.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/noconf_hom.mli
CAMLDEP src/principles_proofs.mli
CAMLDEP src/equations.mli
CAMLDEP src/principles.mli
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
COQDEP src/equations_plugin.mllib
CAMLDEP src/equations_plugin_mod.ml
CAMLDEP src/extra_tactics.ml
CAMLDEP src/noconf.ml
CAMLDEP src/noconf_hom.ml
CAMLDEP src/equations.ml
CAMLDEP src/principles.ml
CAMLDEP src/principles_proofs.ml
CAMLDEP src/covering.ml
CAMLDEP src/splitting.ml
CAMLDEP src/simplify.ml
CAMLDEP src/context_map.ml
CAMLDEP src/syntax.ml
CAMLDEP src/depelim.ml
CAMLDEP src/subterm.ml
CAMLDEP src/sigma_types.ml
CAMLDEP src/ederive.ml
CAMLDEP src/eqdec.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/depelim.mli
CAMLC -c src/context_map.mli
CAMLC -c src/sigma_types.mli
CAMLC -c src/simplify.mli
CAMLC -c src/splitting.mli
CAMLC -c src/covering.mli
CAMLC -c src/principles_proofs.mli
CAMLC -c src/equations.mli
CAMLC -c src/principles.mli
CAMLOPT -c  src/syntax.ml
CAMLOPT -c  src/eqdec.ml
CAMLOPT -c  src/extra_tactics.ml
CAMLOPT -c  src/context_map.ml
CAMLOPT -c  src/sigma_types.ml
CAMLOPT -c  src/simplify.ml
CAMLOPT -c  src/subterm.ml
CAMLOPT -c  src/splitting.ml
CAMLOPT -c  src/covering.ml
CAMLOPT -c  src/depelim.ml
CAMLOPT -c  src/noconf_hom.ml
CAMLOPT -c  src/noconf.ml
CAMLOPT -c  src/principles_proofs.ml
CAMLOPT -c  src/principles.ml
CAMLOPT -c  src/equations.ml
CAMLOPT -c  src/g_equations.ml
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/FunctionalInduction.v
COQC theories/Prop/Constants.v
COQC theories/Prop/TransparentEquations.v
COQC theories/Prop/OpaqueEquations.v
COQC theories/Prop/Subterm.v
COQC theories/Type/DepElim.v
COQC theories/Type/Constants.v
COQC theories/Type/FunctionalInduction.v
COQC theories/Prop/Tactics.v
COQC theories/Type/Subterm.v
COQC theories/Type/Tactics.v
COQC theories/Prop/NoConfusion.v
COQC theories/Type/EqDecInstances.v
COQC theories/Type/NoConfusion.v
COQC theories/Type/Loader.v
COQC theories/Prop/EqDecInstances.v
COQC theories/Type/Telescopes.v
COQC theories/Type/WellFoundedInstances.v
COQC theories/Prop/Loader.v
COQC theories/Type/All.v
COQC theories/Prop/Telescopes.v
COQC theories/Equations.v
phase `build' succeeded after 13.8 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 Noconfinv.v
COQC f91.v
COQC rec.v
COQC zoe.v
COQC gcd.v
COQC DataStruct.v
COQC daaa.v
COQC nestedobls.v
COQC rose.v
COQC scope.v
COQC depelim.v
COQC issues/issue7.v
COQC issues/issue8.v
COQC issues/issue13.v
COQC issues/issue24.v
COQC issues/issue25.v
COQC issues/issue63.v
COQC issues/issue75.v
COQC issues/issue70.v
COQC issues/issue66.v
COQC issues/issue74.v
COQC issues/issue77.v
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
COQC issues/issue100.v
Closed under the global context
Closed under the global context
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
     = 6
     : nat
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/issue246.v
COQC issues/issue249.v
COQC issues/issue258.v
COQC issues/issue286.v
COQC issues/issue297.v
COQC eqdec_error.v
COQC noconf_simplify.v
COQC le.v
COQC LogicType.v
COQC mfix.v
COQC mutrec.v
COQC nestedrec.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 nestedrec2.v
COQC nestfixnorec.v
COQC agda_1408.v
COQC agda_1775.v
COQC tabareau_vec.v
NoConfusion.NoConfusionPackage_list decl : NoConfusionPackage ctx
     : NoConfusionPackage ctx
Program obligation tactic is Tactics.program_simplify;
                              CoreTactics.equations_simpl;
                              try Tactics.program_solve_wf (globally defined)
Closed under the global context
COQC yves.v
COQC local_where.v
COQC cfold.v
COQC nestedwhererec.v
COQC Below.v
COQC divmod.v
COQC fle_trans.v
COQC interval.v
COQC letred.v
COQC nocycle_def.v
COQC nolam.v
COQC issues/issue95_2.v
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]
COQC nocycle.v
Closed under the global context
Axioms:
Eqdep.Eq_rect_eq.eq_rect_eq : forall (U : Type) (p : U) 
                                (Q : U -> Type) (x : Q p) 
                                (h : p = p), x = eq_rect p Q x p h
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y
Closed under the global context
Closed under the global context
Finished transaction in 4.483 secs (4.454u,0.028s) (successful)
Finished transaction in 2.194 secs (2.193u,0.s) (successful)
Closed under the global context
Closed under the global context
COQC Basics.v
COQC innacs.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))))
Finished transaction in 11.082 secs (10.933u,0.147s) (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 32.6 seconds
starting phase `install'
INSTALL theories/Init.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.vo /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.v /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Init.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Signature.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/CoreTactics.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Prop/Logic.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Classes.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDec.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/EqDecInstances.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Subterm.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/DepElim.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Tactics.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Constants.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/NoConfusion.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/FunctionalInduction.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Loader.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/Telescopes.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/TransparentEquations.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Prop/OpaqueEquations.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Prop
INSTALL theories/Equations.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL theories/Type/Logic.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalExtensionality.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Relation_Properties.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFounded.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Classes.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDec.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/DepElim.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Tactics.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Subterm.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Constants.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/EqDecInstances.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/NoConfusion.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/FunctionalInduction.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Loader.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/Telescopes.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/WellFoundedInstances.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL theories/Type/All.glob /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations//Type
INSTALL src/g_equations.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmi /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxs /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin.cmxa /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/g_equations.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_common.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/ederive.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/sigma_types.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/subterm.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/eqdec.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/depelim.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/syntax.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/context_map.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/simplify.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/splitting.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/covering.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles_proofs.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/principles.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf_hom.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/noconf.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/extra_tactics.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-coq-equations-1.2.3/lib/coq//user-contrib/Equations/
INSTALL src/equations_plugin_mod.cmx /gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-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 2.4 seconds
starting phase `patch-shebangs'
phase `patch-shebangs' succeeded after 0.0 seconds
starting phase `strip'
stripping binaries in "/gnu/store/bx15ckyms41wibb06vg5ws5b9y2v1q7l-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/bx15ckyms41wibb06vg5ws5b9y2v1q7l-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