Adjust the way .depend is treated, to fix INSTALLFILES

.gitignore

@@ -20,4 +20,3 @@ interval*/*
 coqopts
 *.crashcoqide
 *.cache
-vcfloat/.depend

vcfloat/.depend

@@ -0,0 +1,62 @@
+Automate.vo Automate.glob Automate.v.beautified Automate.required_vo: Automate.v FPLang.vo FPLangOpt.vo RAux.vo Rounding.vo Reify.vo Float_notations.vo compute_tactics_ltac2.vo
+Automate.vio: Automate.v FPLang.vio FPLangOpt.vio RAux.vio Rounding.vio Reify.vio Float_notations.vio compute_tactics_ltac2.vio
+BigQAux.vo BigQAux.glob BigQAux.v.beautified BigQAux.required_vo: BigQAux.v 
+BigQAux.vio: BigQAux.v 
+BigRAux.vo BigRAux.glob BigRAux.v.beautified BigRAux.required_vo: BigRAux.v BigQAux.vo Q2RAux.vo
+BigRAux.vio: BigRAux.v BigQAux.vio Q2RAux.vio
+FMap_lemmas.vo FMap_lemmas.glob FMap_lemmas.v.beautified FMap_lemmas.required_vo: FMap_lemmas.v 
+FMap_lemmas.vio: FMap_lemmas.v 
+FPCompCert.vo FPCompCert.glob FPCompCert.v.beautified FPCompCert.required_vo: FPCompCert.v FPCore.vo
+FPCompCert.vio: FPCompCert.v FPCore.vio
+FPCore.vo FPCore.glob FPCore.v.beautified FPCore.required_vo: FPCore.v IEEE754_extra.vo klist.vo Float_notations.vo
+FPCore.vio: FPCore.v IEEE754_extra.vio klist.vio Float_notations.vio
+FPLang.vo FPLang.glob FPLang.v.beautified FPLang.required_vo: FPLang.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo Float_lemmas.vo FPCore.vo klist.vo
+FPLang.vio: FPLang.v RAux.vio IEEE754_extra.vio Fprop_absolute.vio Float_lemmas.vio FPCore.vio klist.vio
+FPLangOpt.vo FPLangOpt.glob FPLangOpt.v.beautified FPLangOpt.required_vo: FPLangOpt.v Float_lemmas.vo FPLang.vo klist.vo LibTac.vo BigRAux.vo
+FPLangOpt.vio: FPLangOpt.v Float_lemmas.vio FPLang.vio klist.vio LibTac.vio BigRAux.vio
+FPLib.vo FPLib.glob FPLib.v.beautified FPLib.required_vo: FPLib.v FPCore.vo RAux.vo Rounding.vo Float_notations.vo
+FPLib.vio: FPLib.v FPCore.vio RAux.vio Rounding.vio Float_notations.vio
+Float_lemmas.vo Float_lemmas.glob Float_lemmas.v.beautified Float_lemmas.required_vo: Float_lemmas.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo FPCore.vo
+Float_lemmas.vio: Float_lemmas.v RAux.vio IEEE754_extra.vio Fprop_absolute.vio FPCore.vio
+Float_notations.vo Float_notations.glob Float_notations.v.beautified Float_notations.required_vo: Float_notations.v IEEE754_extra.vo
+Float_notations.vio: Float_notations.v IEEE754_extra.vio
+Fprop_absolute.vo Fprop_absolute.glob Fprop_absolute.v.beautified Fprop_absolute.required_vo: Fprop_absolute.v 
+Fprop_absolute.vio: Fprop_absolute.v 
+IEEE754_extra.vo IEEE754_extra.glob IEEE754_extra.v.beautified IEEE754_extra.required_vo: IEEE754_extra.v 
+IEEE754_extra.vio: IEEE754_extra.v 
+LibTac.vo LibTac.glob LibTac.v.beautified LibTac.required_vo: LibTac.v RAux.vo
+LibTac.vio: LibTac.v RAux.vio
+Prune.vo Prune.glob Prune.v.beautified Prune.required_vo: Prune.v FMap_lemmas.vo
+Prune.vio: Prune.v FMap_lemmas.vio
+Q2RAux.vo Q2RAux.glob Q2RAux.v.beautified Q2RAux.required_vo: Q2RAux.v 
+Q2RAux.vio: Q2RAux.v 
+RAux.vo RAux.glob RAux.v.beautified RAux.required_vo: RAux.v 
+RAux.vio: RAux.v 
+Reify.vo Reify.glob Reify.v.beautified Reify.required_vo: Reify.v RAux.vo IEEE754_extra.vo klist.vo Fprop_absolute.vo Float_lemmas.vo FPCore.vo FPLang.vo Float_notations.vo
+Reify.vio: Reify.v RAux.vio IEEE754_extra.vio klist.vio Fprop_absolute.vio Float_lemmas.vio FPCore.vio FPLang.vio Float_notations.vio
+Rounding.vo Rounding.glob Rounding.v.beautified Rounding.required_vo: Rounding.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo Float_lemmas.vo FPCore.vo FPLang.vo klist.vo
+Rounding.vio: Rounding.v RAux.vio IEEE754_extra.vio Fprop_absolute.vio Float_lemmas.vio FPCore.vio FPLang.vio klist.vio
+Summation.vo Summation.glob Summation.v.beautified Summation.required_vo: Summation.v 
+Summation.vio: Summation.v 
+VCFloat.vo VCFloat.glob VCFloat.v.beautified VCFloat.required_vo: VCFloat.v klist.vo FPLang.vo FPLangOpt.vo RAux.vo Rounding.vo Reify.vo Float_notations.vo Automate.vo Prune.vo Float_notations.vo
+VCFloat.vio: VCFloat.v klist.vio FPLang.vio FPLangOpt.vio RAux.vio Rounding.vio Reify.vio Float_notations.vio Automate.vio Prune.vio Float_notations.vio
+Version.vo Version.glob Version.v.beautified Version.required_vo: Version.v 
+Version.vio: Version.v 
+compute_tactics_ltac2.vo compute_tactics_ltac2.glob compute_tactics_ltac2.v.beautified compute_tactics_ltac2.required_vo: compute_tactics_ltac2.v 
+compute_tactics_ltac2.vio: compute_tactics_ltac2.v 
+klist.vo klist.glob klist.v.beautified klist.required_vo: klist.v 
+klist.vio: klist.v 
+../Test/Test.vo ../Test/Test.glob ../Test/Test.v.beautified ../Test/Test.required_vo: ../Test/Test.v VCFloat.vo
+../Test/Test.vio: ../Test/Test.v VCFloat.vio
+../Test/Test2.vo ../Test/Test2.glob ../Test/Test2.v.beautified ../Test/Test2.required_vo: ../Test/Test2.v VCFloat.vo
+../Test/Test2.vio: ../Test/Test2.v VCFloat.vio
+../Test/TestFunc.vo ../Test/TestFunc.glob ../Test/TestFunc.v.beautified ../Test/TestFunc.required_vo: ../Test/TestFunc.v VCFloat.vo
+../Test/TestFunc.vio: ../Test/TestFunc.v VCFloat.vio
+../Test/TestPaper.vo ../Test/TestPaper.glob ../Test/TestPaper.v.beautified ../Test/TestPaper.required_vo: ../Test/TestPaper.v VCFloat.vo
+../Test/TestPaper.vio: ../Test/TestPaper.v VCFloat.vio
+../Test/TestRefman.vo ../Test/TestRefman.glob ../Test/TestRefman.v.beautified ../Test/TestRefman.required_vo: ../Test/TestRefman.v VCFloat.vo
+../Test/TestRefman.vio: ../Test/TestRefman.v VCFloat.vio
+../Test/autobisect.vo ../Test/autobisect.glob ../Test/autobisect.v.beautified ../Test/autobisect.required_vo: ../Test/autobisect.v VCFloat.vo
+../Test/autobisect.vio: ../Test/autobisect.v VCFloat.vio
+../Test/summation.vo ../Test/summation.glob ../Test/summation.v.beautified ../Test/summation.required_vo: ../Test/summation.v IEEE754_extra.vo VCFloat.vo
+../Test/summation.vio: ../Test/summation.v IEEE754_extra.vio VCFloat.vio

vcfloat/Makefile

@@ -34,17 +34,15 @@ endif
 depend: 
 	$(COQDEP) $(COQFLAGS) *.v ../Test/*.v > .depend
 
-.depend:
-	$(error to build the .depend file: make depend)
-
-all_clean:
-	rm *.vo *.vok *.vos *.glob
-
 ifneq ($(MAKECMDGOALS),depend)
  ifneq ($(MAKECMDGOALS),clean)
   include .depend
  endif
 endif
 
+all_clean:
+	rm *.vo *.vok *.vos *.glob
+
+
 clean:
 	rm -f {*,*/*}.{vo,vo?,glob}