diff --git a/.gitignore b/.gitignore index e312f9d..2c3da02 100644 --- a/.gitignore +++ b/.gitignore @@ -20,4 +20,3 @@ interval*/* coqopts *.crashcoqide *.cache -vcfloat/.depend diff --git a/vcfloat/.depend b/vcfloat/.depend new file mode 100644 index 0000000..68d05cb --- /dev/null +++ b/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 diff --git a/vcfloat/Makefile b/vcfloat/Makefile index eb119d7..062b6bc 100644 --- a/vcfloat/Makefile +++ b/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}