From 711b9d8cdf6e25690d247d9e8c49f005527e64e2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 21 Jul 2017 13:43:31 +0200
Subject: Fixing rewriting in side conditions for "rewrite in *" and "rewrite
 in * |-".

Noticed by Sigurd Schneider.
---
 tactics/tacticals.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'tactics/tacticals.ml')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e7da17cff..0cc0001c1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -408,8 +408,14 @@ module New = struct
     Proofview.tclIFCATCH t1
       (fun () -> tclDISPATCH (Array.to_list a))
       (fun _ -> t3)
+  let tclIFTHENFIRSTELSE t1 t2 t3 =
+    Proofview.tclIFCATCH t1
+      (fun () -> tclEXTEND [t2] (tclUNIT ()) [])
+      (fun _ -> t3)
   let tclIFTHENTRYELSEMUST t1 t2 =
     tclIFTHENELSE t1 (tclTRY t2) t2
+  let tclIFTHENFIRSTTRYELSEMUST t1 t2 =
+    tclIFTHENFIRSTELSE t1 (tclTRY t2) t2
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
-- 
cgit v1.2.3