From 8afac4f87d9d7e3add1c19485f475bd2207bfde7 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Oct 2014 13:43:56 +0200
Subject: Refine tactic: simplify the conclusion only at the end of the tactic.

It was the intended semantics from the beginning. I just wrote it wrong.

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

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