From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 8 Jul 2016 14:43:57 +0200 Subject: Port to Coq 8.5pl2 Manual merging of branch jhjourdan:coq8.5. No other change un functionality. --- flocq/Calc/Fcalc_round.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'flocq') diff --git a/flocq/Calc/Fcalc_round.v b/flocq/Calc/Fcalc_round.v index a1bcb84a..19652d08 100644 --- a/flocq/Calc/Fcalc_round.v +++ b/flocq/Calc/Fcalc_round.v @@ -646,7 +646,7 @@ case Zlt_bool_spec ; intros Hk. (* *) unfold truncate_aux. rewrite Fx at 1. -refine (let H := _ in conj _ H). +unshelve refine (let H := _ in conj _ H). unfold k. ring. rewrite <- H. apply F2R_eq_compat. -- cgit