Fix refine in compatibility mode

1 files changed, 8 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d2e5d8525..548d2a81f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4973,9 +4973,15 @@ module New = struct
   open Locus
 
   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
+      else Some []
+    in
     reduce
-      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=None; concl_occs=AllOccurrences }
+      (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
+	     rZeta=false;rDelta=false;rConst=[]})
+      {onhyps; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
     Refine.refine ?unsafe c <*>