[ssr] use tclDISPATCH for IPatDispatch (fix #8544)

5 files changed, 13 insertions, 10 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 6ba937a2ff..656defef84 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -84,7 +84,7 @@ type ssripat =
   | IPatId of (*TODO id_mod option * *) Id.t
   | IPatAnon of anon_iter (* inaccessible name *)
 (* TODO  | IPatClearMark *)
-  | IPatDispatch of ssripatss (* /[..|..] *)
+  | IPatDispatch of bool (*strict*) * ssripatss (* (..|..) *)
   | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
   | IPatInj of ssripatss
   | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5d75b28539..ebe4aac213 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -800,7 +800,7 @@ let rec is_name_in_ipats name = function
   | IPatId id :: tl -> id = name || 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 ->
+  | (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
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index ce439d0497..71b5b6af3e 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -216,8 +216,11 @@ let rec ipat_tac1 ipat : unit tactic =
   | IPatView (clear_if_id,l) ->
       Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id
         ~conclusion:(fun ~to_clear:clr -> intro_clear clr)
-  | IPatDispatch ipatss ->
-      tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) []
+
+  | IPatDispatch(false,[[]]) ->
+      tclUNIT ()
+  | IPatDispatch(_,ipatss) ->
+      tclDISPATCH (List.map ipat_tac ipatss)
 
   | IPatId id -> Ssrcommon.tclINTRO_ID id
 
@@ -275,7 +278,7 @@ let split_at_first_case ipats =
     loop [] ipats
 
 let ssr_exception is_on = function
-  | Some (IPatCase l) when is_on -> Some (IPatDispatch l)
+  | Some (IPatCase l) when is_on -> Some (IPatDispatch(false, l))
   | x -> x
 
 let option_to_list = function None -> [] | Some x -> [x]
@@ -285,7 +288,7 @@ let elaborate_ipats l =
   let rec elab = function
   | [] -> []
   | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest
-  | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest
+  | IPatDispatch(s,p) :: rest -> IPatDispatch (s,List.map elab p) :: elab rest
   | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest
   | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
   | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ |
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 8699b62c39..52240f5896 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -632,7 +632,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
   | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l)
   | IPatClear clr -> IPatClear (List.map map_ssrhyp clr)
   | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
-  | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
+  | IPatDispatch (s,iorpat) -> IPatDispatch (s,List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
   | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
   | IPatTac _ -> assert false (*internal usage only *)
@@ -697,8 +697,8 @@ let interp_ipat ist gl =
     check_hyps_uniq [] clr'; IPatClear clr'
   | IPatCase(iorpat) ->
       IPatCase(List.map (List.map interp) iorpat)
-  | IPatDispatch(iorpat) ->
-      IPatDispatch(List.map (List.map interp) iorpat)
+  | IPatDispatch(s,iorpat) ->
+      IPatDispatch(s,List.map (List.map interp) iorpat)
   | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
   | IPatAbstractVars l ->
      IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l))
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 8f4b2179e1..824666ba9c 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -101,7 +101,7 @@ let rec pr_ipat p =
   | IPatSimpl sim -> pr_simpl sim
   | IPatClear clr -> pr_clear mt clr
   | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
-  | IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]")
+  | IPatDispatch(_,iorpat) -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]")
   | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]")
   | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir
   | IPatAnon All -> str "*"