Commit 277dd132 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Partly adapt to Coq 8.5.

parent c9694253
...@@ -58,7 +58,7 @@ configure config.status: configure.in ...@@ -58,7 +58,7 @@ configure config.status: configure.in
%.vo: %.v %.vo: %.v
@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@ @COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
@COQC@ -R src Flocq -dont-load-proofs $< @COQC@ -R src Flocq $<
clean: clean:
rm -f $(OBJS) $(EOBJS) src/*.glob examples/*.glob rm -f $(OBJS) $(EOBJS) src/*.glob examples/*.glob
......
...@@ -931,7 +931,6 @@ destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2). ...@@ -931,7 +931,6 @@ destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
rewrite shr_m_shr_record_of_loc. rewrite shr_m_shr_record_of_loc.
intros Hm2. intros Hm2.
rewrite Hm2. rewrite Hm2.
intros z.
repeat split. repeat split.
rewrite Rlt_bool_true. rewrite Rlt_bool_true.
repeat split. repeat split.
...@@ -1482,7 +1481,7 @@ elim Rle_not_lt with (1 := Bz). ...@@ -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). generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy).
intros Bx By (Hx',_) (Hy',_). intros Bx By (Hx',_) (Hy',_).
generalize (canonic_canonic_mantissa sx _ _ Hx') (canonic_canonic_mantissa sy _ _ 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. intros Cx Cy.
destruct sx. destruct sx.
(* ... *) (* ... *)
......
...@@ -222,7 +222,6 @@ Theorem generic_format_FLT_FIX : ...@@ -222,7 +222,6 @@ Theorem generic_format_FLT_FIX :
generic_format beta (FIX_exp emin) x -> generic_format beta (FIX_exp emin) x ->
generic_format beta FLT_exp x. generic_format beta FLT_exp x.
Proof with auto with typeclass_instances. Proof with auto with typeclass_instances.
clear prec_gt_0_.
apply generic_inclusion_le... apply generic_inclusion_le...
intros e He. intros e He.
unfold FIX_exp. unfold FIX_exp.
......
...@@ -182,7 +182,6 @@ Theorem FTZ_format_FLXN : ...@@ -182,7 +182,6 @@ Theorem FTZ_format_FLXN :
(bpow (emin + prec - 1) <= Rabs x)%R -> (bpow (emin + prec - 1) <= Rabs x)%R ->
FLXN_format beta prec x -> FTZ_format x. FLXN_format beta prec x -> FTZ_format x.
Proof. Proof.
clear prec_gt_0_.
intros x Hx Fx. intros x Hx Fx.
apply FTZ_format_generic. apply FTZ_format_generic.
apply generic_format_FLXN in Fx. apply generic_format_FLXN in Fx.
......
...@@ -39,7 +39,7 @@ exists f. ...@@ -39,7 +39,7 @@ exists f.
intros g Hg. intros g Hg.
now apply H2 with (3 := Rle_refl x). 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)). destruct completeness as (f1, (H4, H5)).
simpl. simpl.
destruct H1 as (f2, H1). destruct H1 as (f2, H1).
...@@ -58,7 +58,7 @@ Theorem round_fun_of_pred : ...@@ -58,7 +58,7 @@ Theorem round_fun_of_pred :
{ f : R -> R | forall x, rnd x (f x) }. { f : R -> R | forall x, rnd x (f x) }.
Proof. Proof.
intros rnd H. 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. intros x.
now destruct round_val_of_pred as (f, H1). now destruct round_val_of_pred as (f, H1).
Qed. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment