From 277dd132c480643cffb1ac40f5d2a2d2ef5d7f06 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 3 Dec 2014 10:47:17 +0100
Subject: [PATCH] Partly adapt to Coq 8.5.

---
 Remakefile.in           | 2 +-
 src/Appli/Fappli_IEEE.v | 3 +--
 src/Core/Fcore_FLT.v    | 1 -
 src/Core/Fcore_FTZ.v    | 1 -
 src/Core/Fcore_rnd.v    | 4 ++--
 5 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/Remakefile.in b/Remakefile.in
index fabdc88..6e80643 100644
--- a/Remakefile.in
+++ b/Remakefile.in
@@ -58,7 +58,7 @@ configure config.status: configure.in
 
 %.vo: %.v
 	@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
-	@COQC@ -R src Flocq -dont-load-proofs $<
+	@COQC@ -R src Flocq $<
 
 clean:
 	rm -f $(OBJS) $(EOBJS) src/*.glob examples/*.glob
diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v
index 929a0d8..a1ce046 100644
--- a/src/Appli/Fappli_IEEE.v
+++ b/src/Appli/Fappli_IEEE.v
@@ -931,7 +931,6 @@ destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
 rewrite shr_m_shr_record_of_loc.
 intros Hm2.
 rewrite Hm2.
-intros z.
 repeat split.
 rewrite Rlt_bool_true.
 repeat split.
@@ -1482,7 +1481,7 @@ elim Rle_not_lt with (1 := Bz).
 generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy).
 intros Bx By (Hx',_) (Hy',_).
 generalize (canonic_canonic_mantissa sx _ _ Hx') (canonic_canonic_mantissa sy _ _ Hy').
-clear -Bx By Hs.
+clear -Bx By Hs prec_gt_0_.
 intros Cx Cy.
 destruct sx.
 (* ... *)
diff --git a/src/Core/Fcore_FLT.v b/src/Core/Fcore_FLT.v
index 273ff69..b1a57b6 100644
--- a/src/Core/Fcore_FLT.v
+++ b/src/Core/Fcore_FLT.v
@@ -222,7 +222,6 @@ Theorem generic_format_FLT_FIX :
   generic_format beta (FIX_exp emin) x ->
   generic_format beta FLT_exp x.
 Proof with auto with typeclass_instances.
-clear prec_gt_0_.
 apply generic_inclusion_le...
 intros e He.
 unfold FIX_exp.
diff --git a/src/Core/Fcore_FTZ.v b/src/Core/Fcore_FTZ.v
index 5f3e533..d7e0611 100644
--- a/src/Core/Fcore_FTZ.v
+++ b/src/Core/Fcore_FTZ.v
@@ -182,7 +182,6 @@ Theorem FTZ_format_FLXN :
   (bpow (emin + prec - 1) <= Rabs x)%R ->
   FLXN_format beta prec x -> FTZ_format x.
 Proof.
-clear prec_gt_0_.
 intros x Hx Fx.
 apply FTZ_format_generic.
 apply generic_format_FLXN in Fx.
diff --git a/src/Core/Fcore_rnd.v b/src/Core/Fcore_rnd.v
index 94c9420..171c27f 100644
--- a/src/Core/Fcore_rnd.v
+++ b/src/Core/Fcore_rnd.v
@@ -39,7 +39,7 @@ exists f.
 intros g Hg.
 now apply H2 with (3 := Rle_refl x).
 (* . *)
-exists (projT1 (completeness _ H3 H1)).
+exists (proj1_sig (completeness _ H3 H1)).
 destruct completeness as (f1, (H4, H5)).
 simpl.
 destruct H1 as (f2, H1).
@@ -58,7 +58,7 @@ Theorem round_fun_of_pred :
   { f : R -> R | forall x, rnd x (f x) }.
 Proof.
 intros rnd H.
-exists (fun x => projT1 (round_val_of_pred rnd H x)).
+exists (fun x => proj1_sig (round_val_of_pred rnd H x)).
 intros x.
 now destruct round_val_of_pred as (f, H1).
 Qed.
-- 
GitLab