From 08e87eb96ab67ead60d92394eec6066d9b52e55e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Oct 2014 20:48:38 +0200
Subject: Apparently, the former refine was simplifying in hypotheses too.

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0b7edecac2..0875a76564 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4202,7 +4202,7 @@ module New = struct
   let reduce_after_refine =
     Proofview.V82.tactic (reduce
       (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
-      {onhyps=Some[]; concl_occs=AllOccurrences })
+      {onhyps=None; concl_occs=AllOccurrences })
 
   let refine ?unsafe c =
     Proofview.Refine.refine ?unsafe c <*>
-- 
cgit v1.2.3