From 3ce123f16ce19f67dde4a0f3f2874a2678649907 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Date: Tue, 20 Feb 2018 16:03:57 +0100
Subject: Remove 8.5 compatibility support.

---
 tactics/tactics.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e281e2fe..bf9271ba9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5146,16 +5146,10 @@ module New = struct
   open Locus
 
   let reduce_after_refine =
-    let onhyps =
-      (** We reduced everywhere in the hyps before 8.6 *)
-      if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0
-      then None
-      else Some []
-    in
     reduce
       (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;
 	     rZeta=false;rDelta=false;rConst=[]})
-      {onhyps; concl_occs=AllOccurrences }
+      {onhyps = Some []; concl_occs = AllOccurrences }
 
   let refine ~typecheck c =
     Refine.refine ~typecheck c <*>
-- 
cgit v1.2.3