From dce9ff8da2710aa81fbcf6d1498de35ea9ad06f4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 13 Feb 2017 10:28:35 +0100
Subject: Update Flocq to version 2.5.2

This version of Flocq is compatible with Coq 8.6
---
 flocq/Appli/Fappli_IEEE.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'flocq/Appli/Fappli_IEEE.v')

diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v
index a4accfa5..6400304b 100644
--- a/flocq/Appli/Fappli_IEEE.v
+++ b/flocq/Appli/Fappli_IEEE.v
@@ -1,4 +1,3 @@
-Unset Bracketing Last Introduction Pattern.
 (**
 This file is part of the Flocq formalization of floating-point
 arithmetic in Coq: http://flocq.gforge.inria.fr/
@@ -416,8 +415,7 @@ Theorem is_finite_Bopp :
   forall opp_nan x,
   is_finite (Bopp opp_nan x) = is_finite x.
 Proof.
-intros opp_nan [| | |] ; try easy.
-intros s pl.
+intros opp_nan [| |s pl|] ; try easy.
 simpl.
 now case opp_nan.
 Qed.
@@ -446,8 +444,7 @@ Theorem is_finite_Babs :
   forall abs_nan x,
   is_finite (Babs abs_nan x) = is_finite x.
 Proof.
-  intros abs_nan [| | |] ; try easy.
-  intros s pl.
+  intros abs_nan [| |s pl|] ; try easy.
   simpl.
   now case abs_nan.
 Qed.
-- 
cgit