From f6b297b4c068adadf86e77da533782852cfae373 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 13 Apr 2018 09:59:26 +0200
Subject: [ssr] fix delayed clears (fix #7045)

We take into account all future ipats, not just the ones in
the current branch
---
 plugins/ssr/ssrcommon.ml |  7 +++++--
 plugins/ssr/ssripats.ml  | 19 ++++++++++---------
 2 files changed, 15 insertions(+), 11 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d5118da4c..0522cff03 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -800,8 +800,11 @@ let rec is_name_in_ipats name = function
       List.exists (function SsrHyp(_,id) -> id = name) clr 
       || is_name_in_ipats name tl
   | IPatId id :: tl -> id = name || is_name_in_ipats name tl
-  | (IPatCase l | IPatDispatch l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
-  | _ :: tl -> is_name_in_ipats name tl
+  | IPatAbstractVars ids :: tl ->
+      CList.mem_f Id.equal name ids || is_name_in_ipats name tl
+  | (IPatCase l | IPatDispatch l | IPatInj l) :: tl ->
+      List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl
+  | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl
   | [] -> false
 
 let view_error s gv =
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7897cb170..35036b6cf 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -218,15 +218,16 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
       Ssrview.tclIPAT_VIEWS ~views:l
         ~conclusion:(fun ~to_clear:clr -> intro_clear clr future_ipats)
   | IPatDispatch ipatss ->
-      tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
+      tclEXTEND (List.map (ipat_tac future_ipats) ipatss) (tclUNIT ()) []
 
   | IPatId id -> Ssrcommon.tclINTRO_ID id
 
   | IPatCase ipatss ->
-     tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
+     tclIORPAT (Ssrcommon.tclWITHTOP tac_case) future_ipats ipatss
   | IPatInj ipatss ->
      tclIORPAT (Ssrcommon.tclWITHTOP
-       (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t))) ipatss
+       (fun t -> V82.tactic  ~nf_evars:false (Ssrelim.perform_injection t)))
+       future_ipats ipatss
 
   | IPatAnon Drop -> intro_drop
   | IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -254,17 +255,17 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
 
   | IPatTac t -> t
 
-and ipat_tac pl : unit tactic =
+and ipat_tac future_ipats pl : unit tactic =
   match pl with
   | [] -> tclUNIT ()
   | pat :: pl ->
-      Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 pl)) <*>
+      Ssrcommon.tcl0G (tclLOG pat (ipat_tac1 (pl @ future_ipats))) <*>
       isTICK pat <*>
-      ipat_tac pl
+      ipat_tac future_ipats pl
 
-and tclIORPAT tac = function
+and tclIORPAT tac future_ipats = function
   | [[]] -> tac
-  | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p)
+  | p -> Tacticals.New.tclTHENS tac (List.map (ipat_tac future_ipats) p)
 
 let split_at_first_case ipats =
   let rec loop acc = function
@@ -285,7 +286,7 @@ let main ?eqtac ~first_case_is_dispatch ipats =
   let case = ssr_exception first_case_is_dispatch case in
   let case = option_to_list case in
   let eqtac = option_to_list (Option.map (fun x -> IPatTac x) eqtac) in
-  Ssrcommon.tcl0G (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
+  Ssrcommon.tcl0G (ipat_tac [] (ip_before @ case @ eqtac @ ip_after) <*> intro_end)
 
 end (* }}} *)
 
-- 
cgit v1.2.3