From d8baa76d86eaa691a5386669596a6004bb44bb7a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 18:00:18 +0100
Subject: More precise refine compatibility

---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 92cb8a11ea..af52c52370 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4975,7 +4975,8 @@ module New = struct
   let reduce_after_refine =
     let onhyps =
       (** We reduced everywhere in the hyps before 8.6 *)
-      if Flags.version_less_or_equal Flags.V8_5 then None
+      if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
+      then None
       else Some []
     in
     reduce
-- 
cgit v1.2.3