Use Export instead of Include to access SpecFloat (fix issue #10).

validsdp · Jun 5, 2020 · 709eeb3 · 709eeb3
1 parent 37f69a7
commit 709eeb3
Show file tree

Hide file tree

Showing 9 changed files with 31 additions and 37 deletions.
diff --git a/.gitignore b/.gitignore
@@ -15,7 +15,7 @@ remake.exe
 /html/
 /public/
 src/Version.v
-src/IEEE754/SpecFloat.v
+src/IEEE754/SpecFloatCompat.v
 *.vo
 *.vos
 *.vok

diff --git a/Remakefile.in b/Remakefile.in
@@ -27,7 +27,7 @@ FILES = \
 	Prop/Round_odd.v \
 	Prop/Double_rounding.v \
 	@PRIM_FLOAT@ \
-	IEEE754/SpecFloat.v \
+	IEEE754/SpecFloatCompat.v \
 	IEEE754/BinarySingleNaN.v \
 	IEEE754/Binary.v \
 	IEEE754/Bits.v \
@@ -60,7 +60,7 @@ check: $(EOBJS)
 
 check-more: $(MOBJS)
 
-CONFIGURED_FILES = Remakefile src/Version.v src/IEEE754/SpecFloat.v
+CONFIGURED_FILES = Remakefile src/Version.v src/IEEE754/SpecFloatCompat.v
 
 $(CONFIGURED_FILES): %: %.in config.status
 	./config.status $@
@@ -69,7 +69,7 @@ configure config.status: configure.in
 	autoconf
 	./config.status --recheck
 
-%.vo: %.v | src/IEEE754/SpecFloat.v
+%.vo: %.v | src/IEEE754/SpecFloatCompat.v
 	@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
 	@COQC@ @COQEXTRAFLAGS@ -R src Flocq $<
 

diff --git a/configure.in b/configure.in
@@ -88,5 +88,5 @@ case `$CXX -v 2>&1 | grep -e "^Target:"` in
 	;;
 esac
 
-AC_CONFIG_FILES([Remakefile src/Version.v src/IEEE754/SpecFloat.v])
+AC_CONFIG_FILES([Remakefile src/Version.v src/IEEE754/SpecFloatCompat.v])
 AC_OUTPUT
diff --git a/src/Calc/Bracket.v b/src/Calc/Bracket.v
@@ -20,11 +20,11 @@ COPYING file for more details.
 (** * Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format. *)
 
 Require Import Raux Defs Float_prop.
-Require IEEE754.SpecFloat.
+Require Import SpecFloatCompat.
 
-Notation location := (IEEE754.SpecFloat.location).
-Notation loc_Exact := (IEEE754.SpecFloat.loc_Exact).
-Notation loc_Inexact := (IEEE754.SpecFloat.loc_Inexact).
+Notation location := location (only parsing).
+Notation loc_Exact := loc_Exact (only parsing).
+Notation loc_Inexact := loc_Inexact (only parsing).
 
 Section Fcalc_bracket.
 

diff --git a/src/Core/Digits.v b/src/Core/Digits.v
@@ -17,9 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-Require Import ZArith Zquot.
+From Coq Require Import ZArith Zquot.
+
 Require Import Zaux.
-Require IEEE754.SpecFloat.
+Require Import SpecFloatCompat.
+
+Notation digits2_pos := digits2_pos (only parsing).
+Notation Zdigits2 := Zdigits2 (only parsing).
 
 (** Number of bits (radix 2) of a positive integer.
 
@@ -1119,8 +1123,6 @@ rewrite <- Zpower_nat_Z.
 apply digits2_Pnat_correct.
 Qed.
 
-Local Notation digits2_pos := (IEEE754.SpecFloat.digits2_pos) (only parsing).
-
 Theorem Zpos_digits2_pos :
   forall m : positive,
   Zpos (digits2_pos m) = Zdigits radix2 (Zpos m).
@@ -1133,8 +1135,6 @@ induction m ; simpl ; try easy ;
   apply f_equal, IHm.
 Qed.
 
-Local Notation Zdigits2 := (IEEE754.SpecFloat.Zdigits2) (only parsing).
-
 Lemma Zdigits2_Zdigits :
   forall n, Zdigits2 n = Zdigits radix2 n.
 Proof.
@@ -1143,6 +1143,3 @@ intros [|p|p] ; try easy ;
 Qed.
 
 End Zdigits2.
-
-Notation digits2_pos := (IEEE754.SpecFloat.digits2_pos) (only parsing).
-Notation Zdigits2 := (IEEE754.SpecFloat.Zdigits2) (only parsing).
diff --git a/src/Core/Zaux.v b/src/Core/Zaux.v
@@ -17,9 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-Require Import ZArith Omega.
-Require Import Zquot.
-Require IEEE754.SpecFloat.
+From Coq Require Import ZArith Lia Zquot.
+
+Require Import SpecFloatCompat.
+
+Notation cond_Zopp := cond_Zopp (only parsing).
+Notation iter_pos := iter_pos (only parsing).
 
 Section Zmissing.
 
@@ -703,8 +706,6 @@ End Zcompare.
 
 Section cond_Zopp.
 
-Local Notation cond_Zopp := (IEEE754.SpecFloat.cond_Zopp) (only parsing).
-
 Theorem cond_Zopp_negb :
   forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y).
 Proof.
@@ -736,8 +737,6 @@ Qed.
 
 End cond_Zopp.
 
-Notation cond_Zopp := (IEEE754.SpecFloat.cond_Zopp) (only parsing).
-
 Section fast_pow_pos.
 
 Fixpoint Zfast_pow_pos (v : Z) (e : positive) : Z :=
@@ -924,11 +923,9 @@ intros x.
 apply IHp.
 Qed.
 
-Local Notation iter_pos := (IEEE754.SpecFloat.iter_pos f) (only parsing).
-
 Lemma iter_pos_nat :
   forall (p : positive) (x : A),
-  iter_pos p x = iter_nat (Pos.to_nat p) x.
+  iter_pos f p x = iter_nat (Pos.to_nat p) x.
 Proof.
 induction p ; intros x.
 rewrite Pos2Nat.inj_xI.
@@ -947,5 +944,3 @@ easy.
 Qed.
 
 End Iter.
-
-Notation iter_pos := (IEEE754.SpecFloat.iter_pos) (only parsing).
diff --git a/src/IEEE754/BinarySingleNaN.v b/src/IEEE754/BinarySingleNaN.v
@@ -20,7 +20,7 @@ COPYING file for more details.
 (** * IEEE-754 arithmetic *)
 
 From Coq Require Import Psatz.
-Require Import Core Digits Round Bracket Operations Div Sqrt Relative IEEE754.SpecFloat.
+Require Import Core Digits Round Bracket Operations Div Sqrt Relative SpecFloatCompat.
 
 Definition SF2R beta x :=
   match x with

diff --git a/src/IEEE754/SpecFloat.v.in b/src/IEEE754/SpecFloat.v.in
diff --git a/src/IEEE754/SpecFloatCompat.v.in b/src/IEEE754/SpecFloatCompat.v.in
@@ -0,0 +1,8 @@
+(* Generated from SpecFloatCompat.v.in, *do not edit*. *)
+
+(* This is a compatibility module for Coq < 8.11 which does not provide
+   Coq.Floats.SpecFloat. It should ideally be called SpecFloat but
+   this is not supported by extraction. It is bound to disappear once
+   Flocq requires Coq >= 8.11. *)
+
+Require Export @SPEC_FLOAT_MODULE@.