Merge PR #13659: Make ssr datastructures cpattern and rpattern public

Reviewed-by: gares

12 files changed, 140 insertions, 153 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index f6a741f468..5fbabd7ca1 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -46,7 +46,11 @@ type ssrclear = ssrhyps
 type ssrdocc = ssrclear option * ssrocc
 
 (* OLD ssr terms *)
-type ssrtermkind = char (* FIXME, make algebraic *)
+(* terms are pre constr, the kind is a parsing/printing flag to distinguish
+ * between x, @x and (x). It affects automatic clear and let-in preservation. *)
+(* FIXME *)
+(* Cpattern is a temporary flag that becomes InParens ASAP. *)
+type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
 type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
 
 (* NEW ssr term *)
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 61643c2aa3..37eba7d399 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -19,30 +19,21 @@ open Ssrmatching_plugin
 open Ssrmatching
 
 open Ssrast
-open Ssrprinters
 open Ssrcommon
 
-let char_to_kind = function
-  | '(' -> xInParens
-  | '@' -> xWithAt
-  | ' ' -> xNoFlag
-  | 'x' -> xCpattern
-  | _ -> assert false
-
 (** Backward chaining tactics: apply, exact, congr. *)
 
 (** The "apply" tactic *)
 
 let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
 (* ppdebug(lazy(str"sigma@interp_agen=" ++ pr_evar_map None (project gl))); *)
-  let k = char_to_kind k in
   let rc = pf_intern_term ist gl c in
   let rcs' = rc :: rcs in
   match goclr with
   | None -> clr, rcs'
   | Some ghyps ->
     let clr' = snd (interp_hyps ist gl ghyps) @ clr in
-    if k <> xNoFlag then clr', rcs' else
+    if k <> NoFlag then clr', rcs' else
     let loc = rc.CAst.loc in
     match DAst.get rc with
     | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
@@ -132,7 +123,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
  let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
  let ggenl, tclGENTAC =
    if gviews <> [] && ggenl <> [] then
-     let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
+     let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in
      [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[])))
    else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
  tclGENTAC (fun gl ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cd219838d5..4d57abb465 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -290,7 +290,7 @@ let interp_hyps ist gl ghyps =
 
 (* Old terms *)
 let mk_term k c = k, (mkRHole, Some c)
-let mk_lterm c = mk_term xNoFlag c
+let mk_lterm c = mk_term NoFlag c
 
 (* New terms *)
 
@@ -318,9 +318,9 @@ let interp_ast_closure_term (ist : Geninterp.interp_sign) (gl : 'goal Evd.sigma)
 
 let ssrterm_of_ast_closure_term { body; annotation } =
   let c = match annotation with
-    | `Parens -> xInParens
-    | `At -> xWithAt
-    | _ -> xNoFlag in
+    | `Parens -> InParens
+    | `At -> WithAt
+    | _ -> NoFlag in
   mk_term c body
 
 let ssrdgens_of_parsed_dgens = function
@@ -926,7 +926,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty =
        CProdN (abs, force_type t)
      | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
-     mk_term ' ' (force_type ty) in
+     mk_term NoFlag (force_type ty) in
    let strip_cast (sigma, t) =
      let open EConstr in
      let rec aux t = match kind_of_type sigma t with
@@ -1099,7 +1099,7 @@ let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v)
 
 let interp_clr sigma = function
 | Some clr, (k, c)
-  when (k = xNoFlag  || k = xWithAt) && is_pf_var sigma c ->
+  when (k = NoFlag  || k = WithAt) && is_pf_var sigma c ->
    hyp_of_var sigma c :: clr
 | Some clr, _ -> clr
 | None, _ -> []
@@ -1167,7 +1167,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
   let cl = EConstr.of_constr cl in
   let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in
   if not(occur_existential sigma c) then
-    if tag_of_cpattern t = xWithAt then
+    if tag_of_cpattern t = WithAt then
       if not (EConstr.isVar sigma c) then
         errorstrm (str "@ can be used with variables only")
       else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index fdfba48024..aeb6b3cf85 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -232,7 +232,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with
 
 (* Strip a pattern generated by a prenex implicit to its constant. *)
 let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
-  | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f ->
+  | App (f, a) when kt = NoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f ->
     (sigma, f), true
   | Const _ | Var _ -> p, true
   | Proj _ -> p, true
@@ -736,7 +736,7 @@ let unlocktac ist args =
   Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked ->
   Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key ->
   let ktacs = [
-    (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens);
+    (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) InParens);
     Ssrelim.casetac key (fun ?seed:_ k -> k)
   ] in
   Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 4961138190..f2c7f495b3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -143,8 +143,8 @@ let havetac ist
     let gl, _ = pf_e_type_of gl idty in
     pf_unify_HO gl args_id.(2) abstract_key in
  Tacticals.tclTHENFIRST (Proofview.V82.of_tactic itac_mkabs) (fun gl ->
-  let mkt t = mk_term xNoFlag t in
-  let mkl t = (xNoFlag, (t, None)) in
+  let mkt t = mk_term NoFlag t in
+  let mkl t = (NoFlag, (t, None)) in
   let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in
   let interp_ty gl rtc t =
     let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 46f90a7ee1..1e940b5ad3 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -741,7 +741,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
      [A.. -> Ind] and opens new goals for [A..] as well as for the branches
      of [Ind], see the [~to_ind] argument *)
   if not(Termops.occur_existential sigma c) then
-    if Ssrmatching.tag_of_cpattern t = Ssrprinters.xWithAt then
+    if Ssrmatching.tag_of_cpattern t = Ssrmatching.WithAt then
       if not (EConstr.isVar sigma c) then
         Ssrcommon.errorstrm Pp.(str "@ can be used with variables only")
       else match Context.Named.lookup (EConstr.destVar sigma c) hyps with
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index f06b460ee9..935cef58b9 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -38,6 +38,8 @@ open Constrexpr_ops
 open Proofview
 open Proofview.Notations
 
+open Ssrmatching_plugin.Ssrmatching
+
 open Ssrprinters
 open Ssrcommon
 open Ssrtacticals
@@ -455,9 +457,9 @@ END
 (* Old kinds of terms *)
 
 let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
-  | Tok.KEYWORD "(" -> xInParens
-  | Tok.KEYWORD "@" -> xWithAt
-  | _ -> xNoFlag
+  | Tok.KEYWORD "(" -> InParens
+  | Tok.KEYWORD "@" -> WithAt
+  | _ -> NoFlag
 
 let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
@@ -554,9 +556,9 @@ END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrbwdview;
   ssrbwdview: [
-    [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term xNoFlag c] }
+    [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term NoFlag c] }
     |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> {
-                    (mk_term xNoFlag c) :: w } ]];
+                    (mk_term NoFlag c) :: w } ]];
 END
 
 (* New Views *)
@@ -2201,10 +2203,10 @@ let pr_ssrcongrarg _ _ _ ((n, f), dgens) =
 
 ARGUMENT EXTEND ssrcongrarg TYPED AS ((int * ssrterm) * ssrdgens)
   PRINTED BY { pr_ssrcongrarg }
-| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term xNoFlag c), dgens }
-| [ natural(n) constr(c) ] -> { (n, mk_term xNoFlag c),([[]],[]) }
-| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term xNoFlag c), dgens }
-| [ constr(c) ] -> { (0, mk_term xNoFlag c), ([[]],[]) }
+| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term NoFlag c), dgens }
+| [ natural(n) constr(c) ] -> { (n, mk_term NoFlag c),([[]],[]) }
+| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term NoFlag c), dgens }
+| [ constr(c) ] -> { (0, mk_term NoFlag c), ([[]],[]) }
 END
 
 
@@ -2260,7 +2262,7 @@ let pr_rule = function
 
 let pr_ssrrule _ _ _ = pr_rule
 
-let noruleterm loc = mk_term xNoFlag (mkCProp loc)
+let noruleterm loc = mk_term NoFlag (mkCProp loc)
 
 }
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 95c8024e89..6ed68094dc 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -28,16 +28,6 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
 let pp_term gl t =
   let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
 
-(* FIXME *)
-(* terms are pre constr, the kind is parsing/printing flag to distinguish
- * between x, @x and (x). It affects automatic clear and let-in preservation.
- * Cpattern is a temporary flag that becomes InParens ASAP. *)
-(* type ssrtermkind = InParens | WithAt | NoFlag | Cpattern *)
-let xInParens = '('
-let xWithAt = '@'
-let xNoFlag = ' '
-let xCpattern = 'x'
-
 (* Term printing utilities functions for deciding bracketing.  *)
 let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")")
 (* String lexing utilities *)
@@ -45,10 +35,10 @@ let skip_wschars s =
   let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
 (* We also guard characters that might interfere with the ssreflect   *)
 (* tactic syntax.                                                     *)
-let guard_term ch1 s i = match s.[i] with
+let guard_term kind s i = match s.[i] with
   | '(' -> false
   | '{' | '/' | '=' -> true
-  | _ -> ch1 = xInParens
+  | _ -> kind = Ssrmatching_plugin.Ssrmatching.InParens
 
 (* We also guard characters that might interfere with the ssreflect   *)
 (* tactic syntax.                                                     *)
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 87eb05b667..21fb28038a 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -24,11 +24,6 @@ val pp_concat :
   Pp.t ->
   ?sep:Pp.t -> Pp.t list -> Pp.t
 
-val xInParens : ssrtermkind
-val xWithAt : ssrtermkind
-val xNoFlag : ssrtermkind
-val xCpattern : ssrtermkind
-
 val pr_clear : (unit -> Pp.t) -> ssrclear -> Pp.t
 val pr_clear_ne : ssrclear -> Pp.t
 val pr_dir : ssrdir -> Pp.t
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 2252435658..7022949ab6 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -67,9 +67,9 @@ END
 {
 
 let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
-  | Tok.KEYWORD "(" -> '('
-  | Tok.KEYWORD "@" -> '@'
-  | _ -> ' '
+  | Tok.KEYWORD "(" -> InParens
+  | Tok.KEYWORD "@" -> WithAt
+  | _ -> NoFlag
 let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 }
@@ -78,8 +78,8 @@ GRAMMAR EXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr -> {
     let pattern = mk_term k c None in
-    if loc_of_cpattern pattern <> Some loc && k = '('
-    then mk_term 'x' c None
+    if loc_of_cpattern pattern <> Some loc && k = InParens
+    then mk_term Cpattern c None
     else pattern } ]];
 END
 
@@ -97,8 +97,8 @@ GRAMMAR EXTEND Gram
   GLOBAL: lcpattern;
   lcpattern: [[ k = ssrtermkind; c = lconstr -> {
     let pattern = mk_term k c None in
-    if loc_of_cpattern pattern <> Some loc && k = '('
-    then mk_term 'x' c None
+    if loc_of_cpattern pattern <> Some loc && k = InParens
+    then mk_term Cpattern c None
     else pattern } ]];
 END
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index ea014250ca..2a21049c6e 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -37,6 +37,8 @@ open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
 
+type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern
+
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
 let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
 let ppnl = Feedback.msg_info
@@ -78,10 +80,10 @@ let skip_wschars s =
   let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
 (* We also guard characters that might interfere with the ssreflect   *)
 (* tactic syntax.                                                     *)
-let guard_term ch1 s i = match s.[i] with
+let guard_term kind s i = match s.[i] with
   | '(' -> false
   | '{' | '/' | '=' -> true
-  | _ -> ch1 = '('
+  | _ -> kind = InParens
 (* The call 'guard s i' should return true if the contents of s *)
 (* starting at i need bracketing to avoid ambiguities.          *)
 let pr_guarded guard prc c =
@@ -102,14 +104,6 @@ let prl_glob_constr_and_expr env sigma = function
 let pr_glob_constr_and_expr env sigma = function
   | _, Some c -> pr_constr_expr env sigma c
   | c, None -> pr_glob_constr c
-let pr_term (k, c, _) =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c
-let prl_term (k, c, _) =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c
 
 (** Adding a new uninterpreted generic argument type *)
 let add_genarg tag pr =
@@ -153,28 +147,6 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
 let mkRCast rc rt =  DAst.make @@ GCast (rc, dC rt)
 let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
-(* ssrterm conbinators *)
-let combineCG t1 t2 f g =
- let mk_ist i1 i2 = match i1, i2 with
- | None, Some i -> Some i
- | Some i, None -> Some i
- | None, None -> None
- | Some i, Some j when i == j -> Some i
- | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in
- match t1, t2 with
- | (x, (t1, None), i1), (_, (t2, None), i2) ->
-      x, (g t1 t2, None), mk_ist i1 i2
- | (x, (_, Some t1), i1), (_, (_, Some t2), i2) ->
-      x, (mkRHole, Some (f t1 t2)), mk_ist i1 i2
- | _, (_, (_, None), _) -> CErrors.anomaly (str"have: mixed C-G constr.")
- | _ -> CErrors.anomaly (str"have: mixed G-C constr.")
-let loc_ofCG = function
- | (_, (s, None), _) -> Glob_ops.loc_of_glob_constr s
- | (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s
-
-let mk_term k c ist = k, (mkRHole, Some c), ist
-let mk_lterm = mk_term ' '
-
 let nf_evar sigma c =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
 
@@ -803,25 +775,15 @@ type ('ident, 'term) ssrpattern =
   | E_In_X_In_T of 'term * 'ident * 'term
   | E_As_X_In_T of 'term * 'ident * 'term
 
-let pr_pattern = function
-  | T t -> prl_term t
-  | In_T t -> str "in " ++ prl_term t
-  | X_In_T (x,t) -> prl_term x ++ str " in " ++ prl_term t
-  | In_X_In_T (x,t) -> str "in " ++ prl_term x ++ str " in " ++ prl_term t
+let pr_pattern pr_ident pr_term = function
+  | T t -> pr_term t
+  | In_T t -> str "in " ++ pr_term t
+  | X_In_T (x,t) -> pr_ident x ++ str " in " ++ pr_term t
+  | In_X_In_T (x,t) -> str "in " ++ pr_ident x ++ str " in " ++ pr_term t
   | E_In_X_In_T (e,x,t) ->
-      prl_term e ++ str " in " ++ prl_term x ++ str " in " ++ prl_term t
+      pr_term e ++ str " in " ++ pr_ident x ++ str " in " ++ pr_term t
   | E_As_X_In_T (e,x,t) ->
-      prl_term e ++ str " as " ++ prl_term x ++ str " in " ++ prl_term t
-
-let pr_pattern_w_ids = function
-  | T t -> prl_term t
-  | In_T t -> str "in " ++ prl_term t
-  | X_In_T (x,t) -> pr_id x ++ str " in " ++ prl_term t
-  | In_X_In_T (x,t) -> str "in " ++ pr_id x ++ str " in " ++ prl_term t
-  | E_In_X_In_T (e,x,t) ->
-      prl_term e ++ str " in " ++ pr_id x ++ str " in " ++ prl_term t
-  | E_As_X_In_T (e,x,t) ->
-      prl_term e ++ str " as " ++ pr_id x ++ str " in " ++ prl_term t
+      pr_term e ++ str " as " ++ pr_ident x ++ str " in " ++ pr_term t
 
 let pr_pattern_aux pr_constr = function
   | T t -> pr_constr t
@@ -834,16 +796,53 @@ let pr_pattern_aux pr_constr = function
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern env (sigma, p) =
   pr_pattern_aux (fun t -> pr_econstr_pat env sigma (pi3 (nf_open_term sigma sigma (EConstr.of_constr t)))) p
+
+type cpattern =
+  { kind : ssrtermkind
+  ; pattern : Genintern.glob_constr_and_expr
+  ; interpretation : Geninterp.interp_sign option }
+
+let pr_term {kind; pattern; _} =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pr_guarded (guard_term kind) (pr_glob_constr_and_expr env sigma) pattern
+let prl_term {kind; pattern; _} =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pr_guarded (guard_term kind) (prl_glob_constr_and_expr env sigma) pattern
+
 let pr_cpattern = pr_term
 
-let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern)
+let pr_pattern_w_ids = pr_pattern pr_id prl_term
+
+let mk_term k c ist = {kind=k; pattern=(mkRHole, Some c); interpretation=ist}
+let mk_lterm = mk_term NoFlag
 
 let glob_ssrterm gs = function
-  | k, (_, Some c), None ->
-      let x = Tacintern.intern_constr gs c in
-      k, (fst x, Some c), None
+  | {kind; pattern=(_, Some c); interpretation=None} ->
+    let x = Tacintern.intern_constr gs c in
+    {kind; pattern=(fst x, Some c); interpretation=None}
   | ct -> ct
 
+(* ssrterm conbinators *)
+let combineCG t1 t2 f g =
+  let mk_ist i1 i2 = match i1, i2 with
+    | None, Some i -> Some i
+    | Some i, None -> Some i
+    | None, None -> None
+    | Some i, Some j when i == j -> Some i
+    | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in
+  match t1, t2 with
+  | {kind=x; pattern=(t1, None); interpretation=i1}, {pattern=(t2, None); interpretation=i2} ->
+    {kind=x; pattern=(g t1 t2, None); interpretation = mk_ist i1 i2}
+  | {kind=x; pattern=(_, Some t1); interpretation=i1}, {pattern=(_, Some t2); interpretation=i2} ->
+    {kind=x; pattern=(mkRHole, Some (f t1 t2)); interpretation = mk_ist i1 i2}
+  | _, {pattern=(_, None); _} -> CErrors.anomaly (str"have: mixed C-G constr.")
+  | _ -> CErrors.anomaly (str"have: mixed G-C constr.")
+let loc_ofCG = function
+  | {pattern = (s, None); _} -> Glob_ops.loc_of_glob_constr s
+  | {pattern = (_, Some s); _} -> Constrexpr_ops.constr_loc s
+
 (* This piece of code asserts the following notations are reserved *)
 (* Reserved Notation "( a 'in' b )"        (at level 0).           *)
 (* Reserved Notation "( a 'as' b )"        (at level 0).           *)
@@ -851,19 +850,19 @@ let glob_ssrterm gs = function
 (* Reserved Notation "( a 'as' b 'in' c )" (at level 0).           *)
 let glob_cpattern gs p =
   pp(lazy(str"globbing pattern: " ++ pr_term p));
-  let glob x = pi2 (glob_ssrterm gs (mk_lterm x None)) in
+  let glob x = (glob_ssrterm gs (mk_lterm x None)).pattern in
   let encode k s l =
     let name = Name (Id.of_string ("_ssrpat_" ^ s)) in
-    k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None), None in
+    {kind=k; pattern=(mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None); interpretation=None} in
   let bind_in t1 t2 =
     let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in
     fst (glob (mkCCast mkCHole (mkCLambda n mkCHole t2))) in
   let check_var t2 = if not (isCVar t2) then
     loc_error (constr_loc t2) "Only identifiers are allowed here" in
   match p with
-  | _, (_, None), _ as x -> x
-  | k, (v, Some t), _ as orig ->
-     if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
+  | {pattern = (_, None); _} as x -> x
+  | {kind=k; pattern=(v, Some t); _} as orig ->
+     if k = Cpattern then glob_ssrterm gs {kind=InParens; pattern=(v, Some t); interpretation=None} else
      match t.CAst.v with
      | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) ->
          (try match glob t1, glob t2 with
@@ -891,8 +890,8 @@ let glob_rpattern s p =
   | E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
   | E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
 
-let subst_ssrterm s (k, c, ist) =
-  k, Tacsubst.subst_glob_constr_and_expr s c, ist
+let subst_ssrterm s {kind; pattern; interpretation} =
+  {kind; pattern=Tacsubst.subst_glob_constr_and_expr s pattern; interpretation}
 
 let subst_rpattern s = function
   | T t -> T (subst_ssrterm s t)
@@ -902,7 +901,7 @@ let subst_rpattern s = function
   | E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
   | E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
 
-let interp_ssrterm ist (k,t,_) = k, t, Some ist
+let interp_ssrterm ist {kind; pattern; _} = {kind; pattern; interpretation = Some ist}
 
 let interp_rpattern s = function
   | T t -> T (interp_ssrterm s t)
@@ -910,23 +909,24 @@ let interp_rpattern s = function
   | X_In_T(x,t) -> X_In_T (interp_ssrterm s x,interp_ssrterm s t)
   | In_X_In_T(x,t) -> In_X_In_T (interp_ssrterm s x,interp_ssrterm s t)
   | E_In_X_In_T(e,x,t) ->
-      E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
+    E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
   | E_As_X_In_T(e,x,t) ->
-      E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
+    E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
 
 let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
 
-type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
-let tag_of_cpattern = pi1
+let tag_of_cpattern p = p.kind
 let loc_of_cpattern = loc_ofCG
-let cpattern_of_term (c, t) ist = c, t, Some ist
 type occ = (bool * int list) option
 
 type rpattern = (cpattern, cpattern) ssrpattern
+let pr_rpattern = pr_pattern pr_cpattern pr_cpattern
+
+let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern pr_cpattern pr_cpattern)
 
 type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
-let id_of_cpattern (_, (c1, c2), _) =
+let id_of_cpattern {pattern = (c1, c2); _} =
   let open CAst in
   match DAst.get c1, c2 with
   | _, Some { v = CRef (qid, _) } when qualid_is_ident qid ->
@@ -941,12 +941,12 @@ let id_of_Cterm t = match id_of_cpattern t with
 
 let interp_open_constr ist env sigma gc =
   Tacinterp.interp_open_constr ist env sigma gc
-let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c
+let pf_intern_term env sigma {pattern = c; interpretation = ist; _} = glob_constr ist env sigma c
 
 let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
 
 let interp_term env sigma = function
-  | (_, c, Some ist) ->
+  | {pattern = c; interpretation = Some ist; _} ->
       on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c)
   | _ -> errorstrm (str"interpreting a term with no ist")
 
@@ -974,17 +974,17 @@ let pr_ist { lfun= lfun } =
 *)
 
 let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
-  pp(lazy(str"interpreting: " ++ pr_pattern red));
+  pp(lazy(str"interpreting: " ++ pr_rpattern red));
   let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in
   let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in
   let eAsXInT e x t = E_As_X_In_T(e,x,t) in
-  let mkG ?(k=' ') x ist = k,(x,None), ist in
-  let ist_of (_,_,ist) = ist in
-  let decode (_,_,ist as t) ?reccall f g =
+  let mkG ?(k=NoFlag) x ist = {kind = k; pattern = (x,None); interpretation = ist } in
+  let ist_of x = x.interpretation in
+  let decode ({interpretation=ist; _} as t) ?reccall f g =
     try match DAst.get (pf_intern_term env sigma0 t) with
     | GCast(t,CastConv c) when isGHole t && isGLambda c->
       let (x, c) = destGLambda c in
-      f x (' ',(c,None),ist)
+      f x {kind = NoFlag; pattern = (c,None); interpretation = ist}
     | GVar id
       when Option.has_some ist && let ist = Option.get ist in
            Id.Map.mem id ist.lfun &&
@@ -1027,7 +1027,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
       sigma new_evars in
     sigma in
   let red = let rec decode_red = function
-    | T(k,(t,None),ist) ->
+    | T {kind=k; pattern=(t,None); interpretation=ist} ->
       begin match DAst.get t with
       | GCast (c,CastConv t)
         when isGHole c &&
@@ -1058,7 +1058,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   let red =
     match redty with
     | None -> red
-    | Some (ty, ist) -> let ty = ' ', ty, Some ist in
+    | Some (ty, ist) -> let ty = {kind=NoFlag; pattern=ty; interpretation = Some ist} in
   match red with
   | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
@@ -1072,9 +1072,12 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
       E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | red -> red in
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
-  let mkXLetIn ?loc x (a,(g,c),ist) = match c with
-  | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist
-  | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in
+  let mkXLetIn ?loc x {kind; pattern=(g,c); interpretation} = match c with
+  | Some b -> {kind; pattern=(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)); interpretation}
+  | None -> { kind
+            ; pattern = DAst.make ?loc @@ GLetIn
+                  (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None
+            ; interpretation} in
   match red with
   | T t -> let sigma, t = interp_term env sigma0 t in sigma, T t
   | In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t
@@ -1255,16 +1258,16 @@ let pf_fill_occ_term gl occ t =
   cl, t
 
 let cpattern_of_id id =
-  ' ', (DAst.make @@ GRef (GlobRef.VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })
+  { kind= NoFlag
+  ; pattern = DAst.make @@ GRef (GlobRef.VarRef  id, None), None
+  ; interpretation = Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })}
 
-let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
+let is_wildcard ({pattern = (l, r); _} : cpattern) : bool = match DAst.get l, r with
   | _, Some { CAst.v = CHole _ } | GHole _, None -> true
   | _ -> false
 
 (* "ssrpattern" *)
 
-let pr_rpattern = pr_pattern
-
 let pf_merge_uc uc gl =
   re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc)
 
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 17b47227cb..2b90cef039 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -20,17 +20,16 @@ open Genintern
 
 (** Pattern parsing *)
 
+type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern
+
 (** The type of context patterns, the patterns of the [set] tactic and
     [:] tactical. These are patterns that identify a precise subterm. *)
-type cpattern
+type cpattern =
+  { kind : ssrtermkind
+  ; pattern : Genintern.glob_constr_and_expr
+  ; interpretation : Geninterp.interp_sign option }
 val pr_cpattern : cpattern -> Pp.t
 
-(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
-    These patterns also include patterns that identify all the subterms
-    of a context (i.e. "in" prefix) *)
-type rpattern
-val pr_rpattern : rpattern -> Pp.t
-
 (** Pattern interpretation and matching *)
 
 exception NoMatch
@@ -48,6 +47,12 @@ type ('ident, 'term) ssrpattern =
 type pattern = evar_map * (constr, constr) ssrpattern
 val pp_pattern : env -> pattern -> Pp.t
 
+(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
+    These patterns also include patterns that identify all the subterms
+    of a context (i.e. "in" prefix) *)
+type rpattern = (cpattern, cpattern) ssrpattern
+val pr_rpattern : rpattern -> Pp.t
+
 (** Extracts the redex and applies to it the substitution part of the pattern.
   @raise Anomaly if called on [In_T] or [In_X_In_T] *)
 val redex_of_pattern :
@@ -193,9 +198,6 @@ val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t *
 
 val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t
 
-(* It may be handy to inject a simple term into the first form of cpattern *)
-val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern
-
 (** Helpers to make stateful closures. Example: a [find_P] function may be
     called many times, but the pattern instantiation phase is performed only the
     first time. The corresponding [conclude] has to return the instantiated
@@ -219,7 +221,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma
 
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
-val tag_of_cpattern : cpattern -> char
+val tag_of_cpattern : cpattern -> ssrtermkind
 val loc_of_cpattern : cpattern -> Loc.t option
 val id_of_pattern : pattern -> Names.Id.t option
 val is_wildcard : cpattern -> bool
@@ -245,7 +247,7 @@ sig
   val pr_rpattern : rpattern -> Pp.t
   val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
   val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
-  val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
+  val mk_term : ssrtermkind -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
 
   val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
   val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern