From 925c434592597a34cd7ef4efb5e18a43e197bd96 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Dec 2016 17:25:22 +0100
Subject: Delay use of flag "Discriminate Introduction" from interp to
 execution time.

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index e33dd2e5ed..bb2de1904d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1069,9 +1069,8 @@ let discr with_evars = onEquality with_evars discrEq
 let discrClause with_evars = onClause (discrSimpleClause with_evars)
 
 let discrEverywhere with_evars =
-(*
-  tclORELSE
-*)
+  tclTHEN (Proofview.tclUNIT ())
+    (* Delay the interpretation of side-effect *)
     (if discr_do_intro () then
       (tclTHEN
 	(tclREPEAT introf)
-- 
cgit v1.2.3