Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear all,

I tried to compile the brand new mathcomp-1.6 and I'm running into
trouble. The output show a lot of error messages such as

   mkdir: cannot create directory ‘bkpcoqdep’: File exists
   mv: cannot stat ‘bkpcoqdep/algebra/interval.v’: No such file or directory
   find: ‘bkpcoqdep’: No such file or directory

I attached the output of make. Here is some context informations.  In case you
care: I'm running a Linux OpenSuSE 12.3 distribution on a 64bit machine. My
coq is compiled from the source using the standard Ocaml in my distro:

siteswap-~ $ coqc --version
The Coq Proof Assistant, version 8.4pl5 (July 2015)
compiled on Jul 07 2015 23:22:59 with OCaml 4.02.2

It is installed in /usr/local/bin/coqc which is in the path:

siteswap-~ $ which coqc
/usr/local/bin/coqc

To compile I did:

siteswap-~/src/Coq $ git clone 
:math-comp/math-comp.git
Cloning into 'math-comp'...
remote: Counting objects: 2340, done.
remote: Compressing objects: 100% (106/106), done.
remote: Total 2340 (delta 55), reused 0 (delta 0), pack-reused 2234
Receiving objects: 100% (2340/2340), 5.58 MiB | 137.00 KiB/s, done.
Resolving deltas: 100% (1668/1668), done.
Checking connectivity... done.
siteswap-~/src/Coq $ cd math-comp
siteswap-*rc/Coq/math-comp $ ls
etc  htmldoc  mathcomp  README.md
siteswap-*rc/Coq/math-comp $ cd mathcomp
siteswap-*th-comp/mathcomp $ make >& make.log

Thanks for any help and suggestions.

Cheers,

Florent
Generating Makefile.coq for Coq v8.4 with COQBIN=/usr/local/bin//
# Override COQDEP to find only the "right" copy .ml files
ocamldep -slash -I . "ssrmatching.mli" > "ssrmatching.mli.d" || ( RV=$?; rm 
-f "ssrmatching.mli.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp -c 
"ssreflect.mllib" > "ssreflect.mllib.d" || ( RV=$?; rm -f 
"ssreflect.mllib.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -I . "ssreflect.ml4" > 
"ssreflect.ml4.d" || ( RV=$?; rm -f "ssreflect.ml4.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -I . "ssrmatching.ml4" > 
"ssrmatching.ml4.d" || ( RV=$?; rm -f "ssrmatching.ml4.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/all_algebra.v" > "algebra/all_algebra.v.d" || ( RV=$?; rm -f 
"algebra/all_algebra.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/finalg.v" > "algebra/finalg.v.d" || ( RV=$?; rm -f 
"algebra/finalg.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/fraction.v" > "algebra/fraction.v.d" || ( RV=$?; rm -f 
"algebra/fraction.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/intdiv.v" > "algebra/intdiv.v.d" || ( RV=$?; rm -f 
"algebra/intdiv.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp -c 
ssreflect.mllib
calling coqdep on -exclude-dir plugin -c -slash -I . ssreflect.ml4
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/interval.v" > "algebra/interval.v.d" || ( RV=$?; rm -f 
"algebra/interval.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/matrix.v" > "algebra/matrix.v.d" || ( RV=$?; rm -f 
"algebra/matrix.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/all_algebra.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/intdiv.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/fraction.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/matrix.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/finalg.v
calling coqdep on -exclude-dir plugin -c -slash -I . ssrmatching.ml4
mkdir: mkdir: cannot create directory ‘bkpcoqdep’cannot create directory 
‘bkpcoqdep’: File exists: File exists

calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/interval.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/mxalgebra.v" > "algebra/mxalgebra.v.d" || ( RV=$?; rm -f 
"algebra/mxalgebra.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/mxalgebra.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file algebra/all_algebra.v, 
    required library finalg matches several files in path
    (found finalg.v in algebra and bkpcoqdep/algebra; used the latter)
*** Warning: in file algebra/all_algebra.v, 
    required library intdiv matches several files in path
    (found intdiv.v in algebra and bkpcoqdep/algebra; used the latter)
*** Warning: in file algebra/all_algebra.v, 
    required library interval matches several files in path
    (found interval.v in algebra and bkpcoqdep/algebra; used the latter)
*** Warning: in file algebra/all_algebra.v, 
    required library matrix matches several files in path
    (found matrix.v in algebra and bkpcoqdep/algebra; used the latter)
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/mxpoly.v" > "algebra/mxpoly.v.d" || ( RV=$?; rm -f 
"algebra/mxpoly.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/algebra/interval.v’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
mv: find: cannot stat ‘bkpcoqdep/algebra/mxalgebra.v’../etc/utils/ssrcoqdep 
-exclude-dir plugin -c -slash -R . mathcomp "algebra/polydiv.v" > 
"algebra/polydiv.v.d" || ( RV=$?; rm -f "algebra/polydiv.v.d"; exit ${RV} )
‘bkpcoqdep’calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/mxpoly.v
: No such file or directory
: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/poly.v" > "algebra/poly.v.d" || ( RV=$?; rm -f "algebra/poly.v.d"; 
exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/polyXY.v" > "algebra/polyXY.v.d" || ( RV=$?; rm -f 
"algebra/polyXY.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/polydiv.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/rat.v" > "algebra/rat.v.d" || ( RV=$?; rm -f "algebra/rat.v.d"; exit 
${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/ring_quotient.v" > "algebra/ring_quotient.v.d" || ( RV=$?; rm -f 
"algebra/ring_quotient.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/ssralg.v" > "algebra/ssralg.v.d" || ( RV=$?; rm -f 
"algebra/ssralg.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/poly.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
algebra/ring_quotient.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/polyXY.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/rat.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/ssralg.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/algebra/mxpoly.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/algebra/poly.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/ssrint.v" > "algebra/ssrint.v.d" || ( RV=$?; rm -f 
"algebra/ssrint.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/algebra/rat.v’: No such file or 
directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/ssrnum.v" > "algebra/ssrnum.v.d" || ( RV=$?; rm -f 
"algebra/ssrnum.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/vector.v" > "algebra/vector.v.d" || ( RV=$?; rm -f 
"algebra/vector.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/ssrint.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/ssrnum.v
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/vector.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"algebra/zmodp.v" > "algebra/zmodp.v.d" || ( RV=$?; rm -f 
"algebra/zmodp.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp algebra/zmodp.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file algebra/rat.v, 
    required library ssrnum matches several files in path
    (found ssrnum.v in algebra and bkpcoqdep/algebra; used the latter)
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"all/all.v" > "all/all.v.d" || ( RV=$?; rm -f "all/all.v.d"; exit ${RV} )
find: ‘bkpcoqdep’mv: cannot stat ‘bkpcoqdep/algebra/ssrnum.v’: No such file 
or directory
: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/algebra/ssrint.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/all_character.v" > "character/all_character.v.d" || ( RV=$?; rm -f 
"character/all_character.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/character.v" > "character/character.v.d" || ( RV=$?; rm -f 
"character/character.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/classfun.v" > "character/classfun.v.d" || ( RV=$?; rm -f 
"character/classfun.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp all/all.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/all_character.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/character.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/inertia.v" > "character/inertia.v.d" || ( RV=$?; rm -f 
"character/inertia.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/classfun.v
cp: cannot create regular file ‘bkpcoqdep/character/all_character.v’: No such 
file or directory
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/integral_char.v" > "character/integral_char.v.d" || ( RV=$?; rm -f 
"character/integral_char.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/inertia.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/integral_char.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/character/classfun.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/mxabelem.v" > "character/mxabelem.v.d" || ( RV=$?; rm -f 
"character/mxabelem.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/mxrepresentation.v" > "character/mxrepresentation.v.d" || ( RV=$?; 
rm -f "character/mxrepresentation.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/character/inertia.v’mv: : No such 
file or directorycannot stat ‘bkpcoqdep/character/classfun.v’
: No such file or directory
mv: cannot stat ‘bkpcoqdep/character/classfun.v’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"character/vcharacter.v" > "character/vcharacter.v.d" || ( RV=$?; rm -f 
"character/vcharacter.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/algC.v" > "field/algC.v.d" || ( RV=$?; rm -f "field/algC.v.d"; exit 
${RV} )
find: calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/mxrepresentation.v
‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/algebraics_fundamentals.v" > "field/algebraics_fundamentals.v.d" || ( 
RV=$?; rm -f "field/algebraics_fundamentals.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/algnum.v" > "field/algnum.v.d" || ( RV=$?; rm -f "field/algnum.v.d"; 
exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/algC.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/vcharacter.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
character/mxabelem.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
field/algebraics_fundamentals.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/algnum.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file character/integral_char.v, 
    required library mxrepresentation matches several files in path
    (found mxrepresentation.v in character and bkpcoqdep/character; used the 
latter)
*** Warning: in file character/character.v, 
    required library mxrepresentation matches several files in path
    (found mxrepresentation.v in character and bkpcoqdep/character; used the 
latter)
mv: cannot move ‘bkpcoqdep/character/mxrepresentation.v’ to 
‘character/mxrepresentation.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/character/mxrepresentation.v’: No such file or 
directory
*** Warning: in file character/inertia.v, 
    required library mxrepresentation matches several files in path
    (found mxrepresentation.v in character and bkpcoqdep/character; used the 
latter)
*** Warning: in file character/inertia.v, 
    required library algC matches several files in path
    (found algC.v in field and bkpcoqdep/field; used the latter)
mv: cannot stat ‘bkpcoqdep/character/vcharacter.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/character/mxabelem.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/character/vcharacter.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/algC.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/algC.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/algebraics_fundamentals.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/character/mxabelem.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/all_field.v" > "field/all_field.v.d" || ( RV=$?; rm -f 
"field/all_field.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/closed_field.v" > "field/closed_field.v.d" || ( RV=$?; rm -f 
"field/closed_field.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/field/algC.v’mv: cannot stat 
‘bkpcoqdep/field/algebraics_fundamentals.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/algnum.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/algebraics_fundamentals.v’: No such file or 
directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/countalg.v" > "field/countalg.v.d" || ( RV=$?; rm -f 
"field/countalg.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/cyclotomic.v" > "field/cyclotomic.v.d" || ( RV=$?; rm -f 
"field/cyclotomic.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
field/closed_field.v
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/falgebra.v" > "field/falgebra.v.d" || ( RV=$?; rm -f 
"field/falgebra.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/fieldext.v" > "field/fieldext.v.d" || ( RV=$?; rm -f 
"field/fieldext.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
field/all_field.v
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/finfield.v" > "field/finfield.v.d" || ( RV=$?; rm -f 
"field/finfield.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/countalg.v
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/fieldext.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
field/cyclotomic.v
find: ‘bkpcoqdep’: No such file or directory
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"field/galois.v" > "field/galois.v.d" || ( RV=$?; rm -f "field/galois.v.d"; 
exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’../etc/utils/ssrcoqdep -exclude-dir 
plugin -c -slash -R . mathcomp "field/separable.v" > "field/separable.v.d" || 
( RV=$?; rm -f "field/separable.v.d"; exit ${RV} )
: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/falgebra.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/finfield.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp field/galois.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
field/separable.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file field/all_field.v, 
    required library closed_field matches several files in path
    (found closed_field.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/all_field.v, 
    required library countalg matches several files in path
    (found countalg.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/all_field.v, 
    required library cyclotomic matches several files in path
    (found cyclotomic.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/all_field.v, 
    required library falgebra matches several files in path
    (found falgebra.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/all_field.v, 
    required library fieldext matches several files in path
    (found fieldext.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/all_field.v, 
    required library finfield matches several files in path
    (found finfield.v in field and bkpcoqdep/field; used the latter)
mv: cannot stat ‘bkpcoqdep/field/cyclotomic.v’: No such file or directory
*** Warning: in file field/finfield.v, 
    required library falgebra matches several files in path
    (found falgebra.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/finfield.v, 
    required library fieldext matches several files in path
    (found fieldext.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/finfield.v, 
    required library separable matches several files in path
    (found separable.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/finfield.v, 
    required library galois matches several files in path
    (found galois.v in field and bkpcoqdep/field; used the latter)
*** Warning: in file field/finfield.v, 
    required library cyclotomic matches several files in path
    (found cyclotomic.v in field and bkpcoqdep/field; used the latter)
mv: cannot stat ‘bkpcoqdep/field/falgebra.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/fieldext.v’: No such file or directory
*** Warning: in file field/fieldext.v, 
    required library falgebra matches several files in path
    (found falgebra.v in field and bkpcoqdep/field; used the latter)
mv: cannot stat ‘bkpcoqdep/field/countalg.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/fieldext.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/finfield.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/countalg.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/separable.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/separable.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/galois.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/finfield.v’mv: cannot stat 
‘bkpcoqdep/field/separable.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/finfield.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/action.v" > "fingroup/action.v.d" || ( RV=$?; rm -f 
"fingroup/action.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/field/galois.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/separable.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/all_fingroup.v" > "fingroup/all_fingroup.v.d" || ( RV=$?; rm -f 
"fingroup/all_fingroup.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/field/galois.v’mv: cannot stat 
‘bkpcoqdep/field/galois.v’: No such file or directory
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/automorphism.v" > "fingroup/automorphism.v.d" || ( RV=$?; rm -f 
"fingroup/automorphism.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/fingroup.v" > "fingroup/fingroup.v.d" || ( RV=$?; rm -f 
"fingroup/fingroup.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/gproduct.v" > "fingroup/gproduct.v.d" || ( RV=$?; rm -f 
"fingroup/gproduct.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/morphism.v" > "fingroup/morphism.v.d" || ( RV=$?; rm -f 
"fingroup/morphism.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/perm.v" > "fingroup/perm.v.d" || ( RV=$?; rm -f 
"fingroup/perm.v.d"; exit ${RV} )
find: ‘bkpcoqdep’../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . 
mathcomp "fingroup/presentation.v" > "fingroup/presentation.v.d" || ( RV=$?; 
rm -f "fingroup/presentation.v.d"; exit ${RV} )
: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/all_fingroup.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/quotient.v" > "fingroup/quotient.v.d" || ( RV=$?; rm -f 
"fingroup/quotient.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/fingroup.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/morphism.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/automorphism.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp fingroup/perm.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’mkdir: cannot create directory 
‘bkpcoqdep’: File exists
: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/action.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/presentation.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGappendixAB.v" > "odd_order/BGappendixAB.v.d" || ( RV=$?; rm -f 
"odd_order/BGappendixAB.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’calling coqdep on -exclude-dir 
plugin -c -slash -R . mathcomp fingroup/quotient.v
: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/gproduct.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGappendixAB.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file fingroup/all_fingroup.v, 
    required library action matches several files in path
    (found action.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library automorphism matches several files in path
    (found automorphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library fingroup matches several files in path
    (found fingroup.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library gproduct matches several files in path
    (found gproduct.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library perm matches several files in path
    (found perm.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library presentation matches several files in path
    (found presentation.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/all_fingroup.v, 
    required library quotient matches several files in path
    (found quotient.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/presentation.v, 
    required library fingroup matches several files in path
    (found fingroup.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/presentation.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/perm.v, 
    required library fingroup matches several files in path
    (found fingroup.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/quotient.v, 
    required library fingroup matches several files in path
    (found fingroup.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/quotient.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/quotient.v, 
    required library automorphism matches several files in path
    (found automorphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/gproduct.v, 
    required library fingroup matches several files in path
    (found fingroup.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/gproduct.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/gproduct.v, 
    required library quotient matches several files in path
    (found quotient.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/gproduct.v, 
    required library action matches several files in path
    (found action.v in fingroup and bkpcoqdep/fingroup; used the latter)
mv: cannot stat ‘bkpcoqdep/fingroup/all_fingroup.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/presentation.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/presentation.v’: No such file or directory
*** Warning: in file fingroup/automorphism.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
mv: cannot stat ‘bkpcoqdep/fingroup/action.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/action.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/fingroup.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/automorphism.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/gproduct.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/perm.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/perm.v’: No such file or directory
*** Warning: in file fingroup/action.v, 
    required library morphism matches several files in path
    (found morphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/action.v, 
    required library automorphism matches several files in path
    (found automorphism.v in fingroup and bkpcoqdep/fingroup; used the latter)
*** Warning: in file fingroup/action.v, 
    required library quotient matches several files in path
    (found quotient.v in fingroup and bkpcoqdep/fingroup; used the latter)
mv: cannot stat ‘bkpcoqdep/fingroup/gproduct.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/automorphism.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/all_fingroup.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/quotient.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/all_fingroup.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/quotient.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/gproduct.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’mv: cannot stat 
‘bkpcoqdep/fingroup/morphism.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/presentation.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/presentation.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’mv: cannot stat 
‘bkpcoqdep/odd_order/BGappendixAB.v’: No such file or directory
: No such file or directory
mv: mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’cannot stat 
‘bkpcoqdep/fingroup/action.v’: No such file or directory: No such file or 
directory

mv: cannot stat ‘bkpcoqdep/fingroup/quotient.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGappendixC.v" > "odd_order/BGappendixC.v.d" || ( RV=$?; rm -f 
"odd_order/BGappendixC.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/fingroup/action.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection10.v" > "odd_order/BGsection10.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection10.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’mv: cannot stat 
‘bkpcoqdep/fingroup/automorphism.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/automorphism.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection11.v" > "odd_order/BGsection11.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection11.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection12.v" > "odd_order/BGsection12.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection12.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection13.v" > "odd_order/BGsection13.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection13.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection14.v" > "odd_order/BGsection14.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection14.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/fingroup/gproduct.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/gproduct.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection15.v" > "odd_order/BGsection15.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection15.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection16.v" > "odd_order/BGsection16.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection16.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/fingroup/quotient.v’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection11.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection10.v
mv: cannot stat ‘bkpcoqdep/fingroup/quotient.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’: No such file or directory
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection15.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGappendixC.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection14.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection16.v
mv: cannot stat ‘bkpcoqdep/fingroup/morphism.v’mkdir: cannot create directory 
‘bkpcoqdep’calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection12.v
: File exists
: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection13.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGappendixAB.v’: No such file or 
directory
cp: cannot create regular file ‘bkpcoqdep/odd_order/BGsection10.v’: No such 
file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection1.v" > "odd_order/BGsection1.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection1.v.d"; exit ${RV} )
rm: cannot remove ‘bkpcoqdep’: Directory not empty
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection2.v" > "odd_order/BGsection2.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection2.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection2.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection1.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file odd_order/BGsection16.v, 
    required library BGsection12 matches several files in path
    (found BGsection12.v in odd_order and bkpcoqdep/odd_order; used the 
latter)
*** Warning: in file odd_order/BGsection16.v, 
    required library BGsection13 matches several files in path
    (found BGsection13.v in odd_order and bkpcoqdep/odd_order; used the 
latter)
*** Warning: in file odd_order/BGsection16.v, 
    required library BGsection14 matches several files in path
    (found BGsection14.v in odd_order and bkpcoqdep/odd_order; used the 
latter)
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection14.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection12.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection14.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection1.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection12.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection3.v" > "odd_order/BGsection3.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection3.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection4.v" > "odd_order/BGsection4.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection4.v.d"; exit ${RV} )
*** Warning: in file odd_order/BGsection15.v, 
    required library BGsection1 matches several files in path
    (found BGsection1.v in odd_order and bkpcoqdep/odd_order; used the latter)
*** Warning: in file odd_order/BGsection15.v, 
    required library BGsection12 matches several files in path
    (found BGsection12.v in odd_order and bkpcoqdep/odd_order; used the 
latter)
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection5.v" > "odd_order/BGsection5.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection5.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection6.v" > "odd_order/BGsection6.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection6.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection7.v" > "odd_order/BGsection7.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection7.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection3.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection8.v" > "odd_order/BGsection8.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection8.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection5.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/BGsection9.v" > "odd_order/BGsection9.v.d" || ( RV=$?; rm -f 
"odd_order/BGsection9.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection4.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection6.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection8.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection7.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/BGsection9.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection10.v" > "odd_order/PFsection10.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection10.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection3.v’mkdir: cannot create 
directory ‘bkpcoqdep’: No such file or directory
: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection11.v" > "odd_order/PFsection11.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection11.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/odd_order/BGsection8.v’: No such 
file or directory
find: ‘bkpcoqdep’: No such file or directory
cp: cannot create regular file ‘bkpcoqdep/odd_order/BGsection6.v’: No such 
file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection10.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection11.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection12.v" > "odd_order/PFsection12.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection12.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/odd_order/BGsection9.v’: No such 
file or directory
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection12.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file odd_order/BGsection8.v, 
    required library BGsection7 matches several files in path
    (found BGsection7.v in odd_order and bkpcoqdep/odd_order; used the latter)
mv: cannot stat ‘bkpcoqdep/odd_order/BGsection7.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection10.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection13.v" > "odd_order/PFsection13.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection13.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection12.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection12.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection11.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection14.v" > "odd_order/PFsection14.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection14.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection1.v" > "odd_order/PFsection1.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection1.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection12.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection2.v" > "odd_order/PFsection2.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection2.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection3.v" > "odd_order/PFsection3.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection3.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection4.v" > "odd_order/PFsection4.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection4.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection13.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection14.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection5.v" > "odd_order/PFsection5.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection5.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection1.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection3.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection5.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection2.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection4.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection6.v" > "odd_order/PFsection6.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection6.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection6.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection14.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection3.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection7.v" > "odd_order/PFsection7.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection7.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection1.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection8.v" > "odd_order/PFsection8.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection8.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection8.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection7.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/PFsection9.v" > "odd_order/PFsection9.v.d" || ( RV=$?; rm -f 
"odd_order/PFsection9.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/odd_order/PFsection6.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/stripped_odd_order_theorem.v" > 
"odd_order/stripped_odd_order_theorem.v.d" || ( RV=$?; rm -f 
"odd_order/stripped_odd_order_theorem.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"odd_order/wielandt_fixpoint.v" > "odd_order/wielandt_fixpoint.v.d" || ( 
RV=$?; rm -f "odd_order/wielandt_fixpoint.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/all_real_closed.v" > "real_closed/all_real_closed.v.d" || ( 
RV=$?; rm -f "real_closed/all_real_closed.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/odd_order/PFsection8.v’: No such 
file or directory
cp: cannot create regular file ‘bkpcoqdep/odd_order/PFsection7.v’: No such 
file or directory
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/PFsection9.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/wielandt_fixpoint.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/bigenough.v" > "real_closed/bigenough.v.d" || ( RV=$?; rm -f 
"real_closed/bigenough.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
odd_order/stripped_odd_order_theorem.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/all_real_closed.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/cauchyreals.v" > "real_closed/cauchyreals.v.d" || ( RV=$?; rm -f 
"real_closed/cauchyreals.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/odd_order/PFsection9.v’: No such 
file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/bigenough.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/complex.v" > "real_closed/complex.v.d" || ( RV=$?; rm -f 
"real_closed/complex.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/cauchyreals.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/complex.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/mxtens.v" > "real_closed/mxtens.v.d" || ( RV=$?; rm -f 
"real_closed/mxtens.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/real_closed/cauchyreals.v’: No such 
file or directory
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/real_closed/bigenough.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/real_closed/all_real_closed.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/ordered_qelim.v" > "real_closed/ordered_qelim.v.d" || ( RV=$?; 
rm -f "real_closed/ordered_qelim.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/polyorder.v" > "real_closed/polyorder.v.d" || ( RV=$?; rm -f 
"real_closed/polyorder.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/polyrcf.v" > "real_closed/polyrcf.v.d" || ( RV=$?; rm -f 
"real_closed/polyrcf.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/qe_rcf_th.v" > "real_closed/qe_rcf_th.v.d" || ( RV=$?; rm -f 
"real_closed/qe_rcf_th.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/mxtens.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/ordered_qelim.v
cp: cannot create regular file ‘bkpcoqdep/real_closed/mxtens.v’: No such file 
or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/qe_rcf.v" > "real_closed/qe_rcf.v.d" || ( RV=$?; rm -f 
"real_closed/qe_rcf.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/qe_rcf_th.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/polyorder.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/polyrcf.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"real_closed/realalg.v" > "real_closed/realalg.v.d" || ( RV=$?; rm -f 
"real_closed/realalg.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/abelian.v" > "solvable/abelian.v.d" || ( RV=$?; rm -f 
"solvable/abelian.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/all_solvable.v" > "solvable/all_solvable.v.d" || ( RV=$?; rm -f 
"solvable/all_solvable.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/realalg.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/abelian.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
real_closed/qe_rcf.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/all_solvable.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/alt.v" > "solvable/alt.v.d" || ( RV=$?; rm -f "solvable/alt.v.d"; 
exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/solvable/all_solvable.v’: No such 
file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/burnside_app.v" > "solvable/burnside_app.v.d" || ( RV=$?; rm -f 
"solvable/burnside_app.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp solvable/alt.v
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/burnside_app.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/center.v" > "solvable/center.v.d" || ( RV=$?; rm -f 
"solvable/center.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/commutator.v" > "solvable/commutator.v.d" || ( RV=$?; rm -f 
"solvable/commutator.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/center.v
mv: cannot stat ‘bkpcoqdep/solvable/alt.v’: No such file or directory
mv: mv: cannot stat ‘bkpcoqdep/solvable/alt.v’cannot stat 
‘bkpcoqdep/solvable/alt.v’: No such file or directory: No such file or 
directory

../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/cyclic.v" > "solvable/cyclic.v.d" || ( RV=$?; rm -f 
"solvable/cyclic.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/extraspecial.v" > "solvable/extraspecial.v.d" || ( RV=$?; rm -f 
"solvable/extraspecial.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/extremal.v" > "solvable/extremal.v.d" || ( RV=$?; rm -f 
"solvable/extremal.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/commutator.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/cyclic.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/extraspecial.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/finmodule.v" > "solvable/finmodule.v.d" || ( RV=$?; rm -f 
"solvable/finmodule.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/solvable/center.v’: No such file or 
directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/extremal.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/frobenius.v" > "solvable/frobenius.v.d" || ( RV=$?; rm -f 
"solvable/frobenius.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/finmodule.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/frobenius.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/gfunctor.v" > "solvable/gfunctor.v.d" || ( RV=$?; rm -f 
"solvable/gfunctor.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/gfunctor.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file solvable/center.v, 
    required library cyclic matches several files in path
    (found cyclic.v in solvable and bkpcoqdep/solvable; used the latter)
mv: cannot stat ‘bkpcoqdep/solvable/finmodule.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/frobenius.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/frobenius.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/gseries.v" > "solvable/gseries.v.d" || ( RV=$?; rm -f 
"solvable/gseries.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/solvable/gfunctor.v’: No such file 
or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/hall.v" > "solvable/hall.v.d" || ( RV=$?; rm -f 
"solvable/hall.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/jordanholder.v" > "solvable/jordanholder.v.d" || ( RV=$?; rm -f 
"solvable/jordanholder.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/maximal.v" > "solvable/maximal.v.d" || ( RV=$?; rm -f 
"solvable/maximal.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/jordanholder.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp solvable/hall.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/nilpotent.v" > "solvable/nilpotent.v.d" || ( RV=$?; rm -f 
"solvable/nilpotent.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/gseries.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/pgroup.v" > "solvable/pgroup.v.d" || ( RV=$?; rm -f 
"solvable/pgroup.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/primitive_action.v" > "solvable/primitive_action.v.d" || ( RV=$?; 
rm -f "solvable/primitive_action.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/maximal.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"solvable/sylow.v" > "solvable/sylow.v.d" || ( RV=$?; rm -f 
"solvable/sylow.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/pgroup.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/primitive_action.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
solvable/nilpotent.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp solvable/sylow.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
cp: cannot create regular file ‘bkpcoqdep/solvable/hall.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/all_ssreflect.v" > "ssreflect/all_ssreflect.v.d" || ( RV=$?; rm -f 
"ssreflect/all_ssreflect.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/solvable/gseries.v’: No such file or directory
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/bigop.v" > "ssreflect/bigop.v.d" || ( RV=$?; rm -f 
"ssreflect/bigop.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/all_ssreflect.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/bigop.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file solvable/hall.v, 
    required library pgroup matches several files in path
    (found pgroup.v in solvable and bkpcoqdep/solvable; used the latter)
*** Warning: in file solvable/hall.v, 
    required library nilpotent matches several files in path
    (found nilpotent.v in solvable and bkpcoqdep/solvable; used the latter)
*** Warning: in file solvable/hall.v, 
    required library sylow matches several files in path
    (found sylow.v in solvable and bkpcoqdep/solvable; used the latter)
*** Warning: in file solvable/maximal.v, 
    required library pgroup matches several files in path
    (found pgroup.v in solvable and bkpcoqdep/solvable; used the latter)
*** Warning: in file solvable/maximal.v, 
    required library nilpotent matches several files in path
    (found nilpotent.v in solvable and bkpcoqdep/solvable; used the latter)
*** Warning: in file solvable/maximal.v, 
    required library sylow matches several files in path
    (found sylow.v in solvable and bkpcoqdep/solvable; used the latter)
mv: cannot stat ‘bkpcoqdep/solvable/pgroup.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/nilpotent.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/all_ssreflect.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/solvable/primitive_action.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/solvable/primitive_action.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssreflect/all_ssreflect.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssreflect/bigop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/sylow.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/sylow.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/nilpotent.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/all_ssreflect.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/binomial.v" > "ssreflect/binomial.v.d" || ( RV=$?; rm -f 
"ssreflect/binomial.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/solvable/primitive_action.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/choice.v" > "ssreflect/choice.v.d" || ( RV=$?; rm -f 
"ssreflect/choice.v.d"; exit ${RV} )
find: ‘bkpcoqdep’../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . 
mathcomp "ssreflect/div.v" > "ssreflect/div.v.d" || ( RV=$?; rm -f 
"ssreflect/div.v.d"; exit ${RV} )
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/eqtype.v" > "ssreflect/eqtype.v.d" || ( RV=$?; rm -f 
"ssreflect/eqtype.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssreflect/all_ssreflect.v’mv: : No such file or 
directorycannot stat ‘bkpcoqdep/solvable/sylow.v’
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/finfun.v" > "ssreflect/finfun.v.d" || ( RV=$?; rm -f 
"ssreflect/finfun.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/fingraph.v" > "ssreflect/fingraph.v.d" || ( RV=$?; rm -f 
"ssreflect/fingraph.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/finset.v" > "ssreflect/finset.v.d" || ( RV=$?; rm -f 
"ssreflect/finset.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/choice.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/fintype.v" > "ssreflect/fintype.v.d" || ( RV=$?; rm -f 
"ssreflect/fintype.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssreflect/all_ssreflect.v’: No such file or 
directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/binomial.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/eqtype.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssreflect/div.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/generic_quotient.v" > "ssreflect/generic_quotient.v.d" || ( RV=$?; 
rm -f "ssreflect/generic_quotient.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/finset.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/finfun.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/fingraph.v
mkdir: mkdir: cannot create directory ‘bkpcoqdep’cannot create directory 
‘bkpcoqdep’: File exists
: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/generic_quotient.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/fintype.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/path.v" > "ssreflect/path.v.d" || ( RV=$?; rm -f 
"ssreflect/path.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssreflect/path.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file ssreflect/finfun.v, 
    required library fintype matches several files in path
    (found fintype.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
mv: cannot stat ‘bkpcoqdep/ssreflect/path.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/prime.v" > "ssreflect/prime.v.d" || ( RV=$?; rm -f 
"ssreflect/prime.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/seq.v" > "ssreflect/seq.v.d" || ( RV=$?; rm -f 
"ssreflect/seq.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/ssrbool.v" > "ssreflect/ssrbool.v.d" || ( RV=$?; rm -f 
"ssreflect/ssrbool.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/ssreflect.v" > "ssreflect/ssreflect.v.d" || ( RV=$?; rm -f 
"ssreflect/ssreflect.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
find: calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/ssrbool.v
‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/ssrfun.v" > "ssreflect/ssrfun.v.d" || ( RV=$?; rm -f 
"ssreflect/ssrfun.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssreflect/seq.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/prime.v
rm: cannot remove ‘bkpcoqdep’: Is a directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/ssrmatching.v" > "ssreflect/ssrmatching.v.d" || ( RV=$?; rm -f 
"ssreflect/ssrmatching.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/ssreflect.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/ssrmatching.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/ssrnat.v" > "ssreflect/ssrnat.v.d" || ( RV=$?; rm -f 
"ssreflect/ssrnat.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/ssreflect/ssrbool.v’: No such file 
or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/ssrfun.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/tuple.v" > "ssreflect/tuple.v.d" || ( RV=$?; rm -f 
"ssreflect/tuple.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’mkdir: cannot create directory 
‘bkpcoqdep’: File exists
: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/absevarprop.v" > "ssrtest/absevarprop.v.d" || ( RV=$?; rm -f 
"ssrtest/absevarprop.v.d"; exit ${RV} )
cp: cannot create regular file ‘bkpcoqdep/ssreflect/seq.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/binders_of.v" > "ssrtest/binders_of.v.d" || ( RV=$?; rm -f 
"ssrtest/binders_of.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/ssrnat.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/absevarprop.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/tuple.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’calling coqdep on -exclude-dir 
plugin -c -slash -R . mathcomp ssrtest/binders_of.v
: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
*** Warning: in file ssreflect/prime.v, 
    required library ssrfun matches several files in path
    (found ssrfun.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssreflect/ssreflect.v, 
    required library ssrmatching matches several files in path
    (found ssrmatching.v in ssreflect and bkpcoqdep/ssreflect; used the 
latter)
*** Warning: in file ssreflect/ssrbool.v, 
    required library ssrfun matches several files in path
    (found ssrfun.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssreflect/ssrfun.v, 
    required library ssreflect matches several files in path
    (found ssreflect.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrmatching.v’: No such file or directory
*** Warning: in file ssrtest/absevarprop.v, 
    required library ssrfun matches several files in path
    (found ssrfun.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssrtest/absevarprop.v, 
    required library ssrnat matches several files in path
    (found ssrnat.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssreflect/tuple.v, 
    required library ssrfun matches several files in path
    (found ssrfun.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssreflect/tuple.v, 
    required library ssrnat matches several files in path
    (found ssrnat.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrfun.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrfun.v’*** Warning: in file 
ssreflect/seq.v, 
    required library ssrfun matches several files in path
    (found ssrfun.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
*** Warning: in file ssreflect/seq.v, 
    required library ssrnat matches several files in path
    (found ssrnat.v in ssreflect and bkpcoqdep/ssreflect; used the latter)
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrfun.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrnat.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrnat.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrnat.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrnat.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/ssrnat.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/tuple.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/tuple.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/tuple.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssreflect/tuple.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/binders.v" > "ssrtest/binders.v.d" || ( RV=$?; rm -f 
"ssrtest/binders.v.d"; exit ${RV} )
mv: mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’cannot stat 
‘bkpcoqdep/ssreflect/tuple.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’find: ‘bkpcoqdep’: No such 
file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/absevarprop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/binders_of.v’: No such file or directory
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/caseview.v" > "ssrtest/caseview.v.d" || ( RV=$?; rm -f 
"ssrtest/caseview.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/congr.v" > "ssrtest/congr.v.d" || ( RV=$?; rm -f 
"ssrtest/congr.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders_of.v’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/binders.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/deferclear.v" > "ssrtest/deferclear.v.d" || ( RV=$?; rm -f 
"ssrtest/deferclear.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/dependent_type_err.v" > "ssrtest/dependent_type_err.v.d" || ( RV=$?; 
rm -f "ssrtest/dependent_type_err.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/elim2.v" > "ssrtest/elim2.v.d" || ( RV=$?; rm -f 
"ssrtest/elim2.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/caseview.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/elim_pattern.v" > "ssrtest/elim_pattern.v.d" || ( RV=$?; rm -f 
"ssrtest/elim_pattern.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/elim.v" > "ssrtest/elim.v.d" || ( RV=$?; rm -f "ssrtest/elim.v.d"; 
exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/congr.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/first_n.v" > "ssrtest/first_n.v.d" || ( RV=$?; rm -f 
"ssrtest/first_n.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/deferclear.v
mkdir: ../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/gen_have.v" > "ssrtest/gen_have.v.d" || ( RV=$?; rm -f 
"ssrtest/gen_have.v.d"; exit ${RV} )
cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/elim2.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/dependent_type_err.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/elim_pattern.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/gen_have.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/first_n.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/elim.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/ssrtest/binders.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/binders.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/congr.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/congr.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/congr.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/deferclear.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/deferclear.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/deferclear.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’: No such file or directory
mv: mv: cannot stat ‘bkpcoqdep/ssrtest/caseview.v’cannot stat 
‘bkpcoqdep/ssrtest/dependent_type_err.v’: No such file or directory: No such 
file or directory

mv: cannot stat ‘bkpcoqdep/ssrtest/dependent_type_err.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/dependent_type_err.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/dependent_type_err.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/dependent_type_err.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/dependent_type_err.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim2.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/elim_pattern.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/gen_pattern.v" > "ssrtest/gen_pattern.v.d" || ( RV=$?; rm -f 
"ssrtest/gen_pattern.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_have.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/havesuff.v" > "ssrtest/havesuff.v.d" || ( RV=$?; rm -f 
"ssrtest/havesuff.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/elim.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/have_TC.v" > "ssrtest/have_TC.v.d" || ( RV=$?; rm -f 
"ssrtest/have_TC.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/elim.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/have_transp.v" > "ssrtest/have_transp.v.d" || ( RV=$?; rm -f 
"ssrtest/have_transp.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/first_n.v’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/elim.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/have_view_idiom.v" > "ssrtest/have_view_idiom.v.d" || ( RV=$?; rm -f 
"ssrtest/have_view_idiom.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/if_isnt.v" > "ssrtest/if_isnt.v.d" || ( RV=$?; rm -f 
"ssrtest/if_isnt.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/elim.v’calling coqdep on -exclude-dir 
plugin -c -slash -R . mathcomp ssrtest/gen_pattern.v
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/indetLHS.v" > "ssrtest/indetLHS.v.d" || ( RV=$?; rm -f 
"ssrtest/indetLHS.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/intro_beta.v" > "ssrtest/intro_beta.v.d" || ( RV=$?; rm -f 
"ssrtest/intro_beta.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/havesuff.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/intro_noop.v" > "ssrtest/intro_noop.v.d" || ( RV=$?; rm -f 
"ssrtest/intro_noop.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/have_TC.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/ipatalternation.v" > "ssrtest/ipatalternation.v.d" || ( RV=$?; rm -f 
"ssrtest/ipatalternation.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/have_transp.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/have_view_idiom.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/intro_noop.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/intro_beta.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/if_isnt.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/ipatalternation.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/indetLHS.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/ssrtest/gen_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/have_TC.v’: No such file or directory
mv: mv: cannot stat ‘bkpcoqdep/ssrtest/if_isnt.v’cannot stat 
‘bkpcoqdep/ssrtest/if_isnt.v’: No such file or directory: No such file or 
directory

mv: cannot stat ‘bkpcoqdep/ssrtest/have_transp.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/if_isnt.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_noop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/have_view_idiom.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_noop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_noop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or 
directorymv: 
cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/havesuff.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/indetLHS.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_noop.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/if_isnt.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/indetLHS.v’: No such file or directory
: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/ltac_have.v" > "ssrtest/ltac_have.v.d" || ( RV=$?; rm -f 
"ssrtest/ltac_have.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/indetLHS.v’mv: find: cannot stat 
‘bkpcoqdep/ssrtest/indetLHS.v’‘bkpcoqdep’: No such file or directory
: No such file or directory: No such file or directory

mv: cannot stat ‘bkpcoqdep/ssrtest/indetLHS.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_noop.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/ltac_in.v" > "ssrtest/ltac_in.v.d" || ( RV=$?; rm -f 
"ssrtest/ltac_in.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/move_after.v" > "ssrtest/move_after.v.d" || ( RV=$?; rm -f 
"ssrtest/move_after.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/multiview.v" > "ssrtest/multiview.v.d" || ( RV=$?; rm -f 
"ssrtest/multiview.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/ltac_have.v
mv: cannot stat ‘bkpcoqdep/ssrtest/indetLHS.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/occarrow.v" > "ssrtest/occarrow.v.d" || ( RV=$?; rm -f 
"ssrtest/occarrow.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/ltac_in.v
mv: cannot stat ‘bkpcoqdep/ssrtest/intro_beta.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/patnoX.v" > "ssrtest/patnoX.v.d" || ( RV=$?; rm -f 
"ssrtest/patnoX.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’../etc/utils/ssrcoqdep 
-exclude-dir plugin -c -slash -R . mathcomp "ssrtest/rewpatterns.v" > 
"ssrtest/rewpatterns.v.d" || ( RV=$?; rm -f "ssrtest/rewpatterns.v.d"; exit 
${RV} )
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/move_after.v
mv: cannot stat ‘bkpcoqdep/ssrtest/indetLHS.v’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/multiview.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/occarrow.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/set_lamda.v" > "ssrtest/set_lamda.v.d" || ( RV=$?; rm -f 
"ssrtest/set_lamda.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/patnoX.v
mv: cannot stat ‘bkpcoqdep/ssrtest/ipatalternation.v’: No such file or 
directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/rewpatterns.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/set_pattern.v" > "ssrtest/set_pattern.v.d" || ( RV=$?; rm -f 
"ssrtest/set_pattern.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
cp: cannot create regular file ‘bkpcoqdep/ssrtest/ltac_have.v’: No such file 
or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/ssrsyntax1.v" > "ssrtest/ssrsyntax1.v.d" || ( RV=$?; rm -f 
"ssrtest/ssrsyntax1.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/set_lamda.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/set_pattern.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/ssrsyntax1.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/ssrtest/patnoX.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/patnoX.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/patnoX.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/rewpatterns.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/multiview.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/rewpatterns.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/multiview.v’: No such file or directory
mv: mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’cannot stat 
‘bkpcoqdep/ssrtest/rewpatterns.v’: No such file or directory: No such file or 
directory

mv: cannot stat ‘bkpcoqdep/ssrtest/rewpatterns.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/multiview.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/multiview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/multiview.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_pattern.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/ssrsyntax2.v" > "ssrtest/ssrsyntax2.v.d" || ( RV=$?; rm -f 
"ssrtest/ssrsyntax2.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/set_pattern.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_lamda.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/set_pattern.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/tc.v" > "ssrtest/tc.v.d" || ( RV=$?; rm -f "ssrtest/tc.v.d"; exit 
${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/set_pattern.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/set_pattern.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/testmx.v" > "ssrtest/testmx.v.d" || ( RV=$?; rm -f 
"ssrtest/testmx.v.d"; exit ${RV} )
mv: cannot stat ‘bkpcoqdep/ssrtest/ssrsyntax1.v’: No such file or directory
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/ssrsyntax2.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/typeof.v" > "ssrtest/typeof.v.d" || ( RV=$?; rm -f 
"ssrtest/typeof.v.d"; exit ${RV} )
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/unkeyed.v" > "ssrtest/unkeyed.v.d" || ( RV=$?; rm -f 
"ssrtest/unkeyed.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/tc.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/view_case.v" > "ssrtest/view_case.v.d" || ( RV=$?; rm -f 
"ssrtest/view_case.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/testmx.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/wlogletin.v" > "ssrtest/wlogletin.v.d" || ( RV=$?; rm -f 
"ssrtest/wlogletin.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/wlog_suff.v" > "ssrtest/wlog_suff.v.d" || ( RV=$?; rm -f 
"ssrtest/wlog_suff.v.d"; exit ${RV} )
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssrtest/wlong_intro.v" > "ssrtest/wlong_intro.v.d" || ( RV=$?; rm -f 
"ssrtest/wlong_intro.v.d"; exit ${RV} )
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/unkeyed.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp ssrtest/typeof.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/view_case.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/wlogletin.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/wlog_suff.v
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssrtest/wlong_intro.v
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mkdir: cannot create directory ‘bkpcoqdep’: File exists
mv: cannot stat ‘bkpcoqdep/ssrtest/typeof.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/view_case.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/view_case.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlog_suff.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlog_suff.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlog_suff.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlogletin.v’mv: cannot stat 
‘bkpcoqdep/ssrtest/wlogletin.v’: No such file or directory
: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlogletin.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlogletin.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlogletin.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlong_intro.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlong_intro.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlong_intro.v’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlong_intro.v’: No such file or directory
mv: cannot stat ‘bkpcoqdep/ssrtest/wlong_intro.v’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
find: ‘bkpcoqdep’: No such file or directory
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"fingroup/presentation.v" > "fingroup/presentation.v.d" || ( RV=$?; rm -f 
"fingroup/presentation.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
fingroup/presentation.v
../etc/utils/ssrcoqdep -exclude-dir plugin -c -slash -R . mathcomp 
"ssreflect/finset.v" > "ssreflect/finset.v.d" || ( RV=$?; rm -f 
"ssreflect/finset.v.d"; exit ${RV} )
calling coqdep on -exclude-dir plugin -c -slash -R . mathcomp 
ssreflect/finset.v
make[1]: *** No rule to make target 'bkpcoqdep/ssreflect/ssrmatching.vo', 
needed by 'ssreflect/ssreflect.vo'.  Stop.
Makefile:24: recipe for target 'all' failed
make: *** [all] Error 2