ssr: rewrite Ssripats and Ssrview in the tactic monad

Ssripats and Ssrview are now written in the Tactic Monad.
Ssripats implements the => tactical.
Ssrview implements the application of forward views.

The code is, according to my tests, 100% backward compatible.
The code is much more documented than before.
Moreover the "ist" (ltac context) used to interpret views is the correct
one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC
EXTEND execution time).  Some of the code not touched by this commit
still uses the incorrect ist, so its visibility in TACTIC EXTEND
can't be removed yet.

The main changes in the code are:
- intro patterns are implemented using a state machine (a goal comes
  with a state). Ssrcommon.MakeState provides an easy way for a tactic
  to enrich the goal with with data of interest, such as the set of
  hyps to be cleared.  This cleans up the old implementation that, in
  order to thread the state, that to redefine a bunch of tclSTUFF
- the interpretation of (multiple) forward views uses the state to
  accumulate intermediate results
- the bottom of Sscommon collects a bunch of utilities written in the
  tactic monad. Most of them are the rewriting of already existing
  utilities.  When possible the old version was removed.

2 files changed, 133 insertions, 97 deletions

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index d05f50e6d..f8d78d2c8 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -73,12 +73,13 @@ let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind c with App (f, a) -> f, a | _ -> c, [| |]
 (* Toplevel constr must be globalized twice ! *)
-let glob_constr ist genv sigma = function
-  | _, Some ce ->
+let glob_constr ist genv sigma t = match t, ist with
+  | (_, Some ce), Some ist ->
     let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in
     let ltacvars = { Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in
     Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv sigma ce
-  | rc, None -> rc
+  | (rc, None), _ -> rc
+  | (_, Some _), None -> CErrors.anomaly Pp.(str"glob_constr: term with no ist")
 
 (* Term printing utilities functions for deciding bracketing.  *)
 let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")")
@@ -107,8 +108,8 @@ let prl_glob_constr_and_expr = function
 let pr_glob_constr_and_expr = function
   | _, Some c -> pr_constr_expr c
   | c, None -> pr_glob_constr c
-let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
-let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c
+let pr_term (k, c, _) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
+let prl_term (k, c, _) = pr_guarded (guard_term k) prl_glob_constr_and_expr c
 
 (** Adding a new uninterpreted generic argument type *)
 let add_genarg tag pr =
@@ -148,16 +149,25 @@ 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 = match t1, t2 with
- | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
- | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2))
- | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr.")
+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
+ | (_, (s, None), _) -> Glob_ops.loc_of_glob_constr s
+ | (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s
 
-let mk_term k c = k, (mkRHole, Some c)
+let mk_term k c ist = k, (mkRHole, Some c), ist
 let mk_lterm = mk_term ' '
 
 let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl)  sigma, ty
@@ -890,9 +900,9 @@ let pr_rpattern _ _ _ = pr_pattern
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
-  | k, (_, Some c) -> k,
+  | k, (_, Some c), None ->
       let x = Tacintern.intern_constr gs c in
-      fst x, Some c
+      k, (fst x, Some c), None
   | ct -> ct
 
 (* This piece of code asserts the following notations are reserved *)
@@ -902,19 +912,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 = snd (glob_ssrterm gs (mk_lterm x)) in
+  let glob x = pi2 (glob_ssrterm gs (mk_lterm x None)) 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) in
+    k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None), 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)) else
+  | _, (_, None), _ as x -> x
+  | k, (v, Some t), _ as orig ->
+     if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
      match t.CAst.v with
      | CNotation("( _ in _ )", ([t1; t2], [], [], [])) ->
          (try match glob t1, glob t2 with
@@ -942,7 +952,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) = k, Tacsubst.subst_glob_constr_and_expr s c
+let subst_ssrterm s (k, c, ist) =
+  k, Tacsubst.subst_glob_constr_and_expr s c, ist
 
 let subst_rpattern s = function
   | T t -> T (subst_ssrterm s t)
@@ -952,37 +963,53 @@ 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_rpattern s = function
+  | T t -> T (interp_ssrterm s t)
+  | In_T t -> In_T (interp_ssrterm s t)
+  | 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_As_X_In_T(e,x,t) ->
+      E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
+
+let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t
+
 ARGUMENT EXTEND rpattern
   TYPED AS rpatternty
   PRINTED BY pr_rpattern
+  INTERPRETED BY interp_rpattern
   GLOBALIZED BY glob_rpattern
   SUBSTITUTED BY subst_rpattern
-  | [ lconstr(c) ] -> [ T (mk_lterm c) ]
-  | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c) ]
+  | [ lconstr(c) ] -> [ T (mk_lterm c None) ]
+  | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ]
   | [ lconstr(x) "in" lconstr(c) ] -> 
-    [ X_In_T (mk_lterm x, mk_lterm c) ]
+    [ X_In_T (mk_lterm x None, mk_lterm c None) ]
   | [ "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ In_X_In_T (mk_lterm x, mk_lterm c) ]
+    [ In_X_In_T (mk_lterm x None, mk_lterm c None) ]
   | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_In_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ]
+    [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
   | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_As_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ]
+    [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
 END
 
 
 
-type cpattern = char * glob_constr_and_expr
-let tag_of_cpattern = fst
+type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option
+let tag_of_cpattern = pi1
 let loc_of_cpattern = loc_ofCG
-let cpattern_of_term t = t
+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
 
 type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
-let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with
+let id_of_cpattern (_, (c1, c2), _) =
+  let open CAst in
+  match DAst.get c1, c2 with
   | _, Some { v = CRef (Ident (_, x), _) } -> Some x
   | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x
   | GRef (VarRef x, _), None -> Some x
@@ -1009,8 +1036,7 @@ let interp_wit wit ist gl x =
   sigma, Value.cast (topwit wit) arg
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
-let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) gl.sigma c
-let interp_term ist gl (_, c) = on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
+let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c
 let pr_ssrterm _ _ _ = pr_term
 let input_ssrtermkind strm = match stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
@@ -1018,7 +1044,7 @@ let input_ssrtermkind strm = match stream_nth 0 strm with
   | _ -> ' '
 let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
-let interp_ssrterm _ gl t = Tacmach.project gl, t
+let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
 
 ARGUMENT EXTEND cpattern
      PRINTED BY pr_ssrterm
@@ -1026,14 +1052,16 @@ ARGUMENT EXTEND cpattern
      GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
      RAW_PRINTED BY pr_ssrterm
      GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" constr(c) ] -> [ mk_lterm c ]
+| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
 END
 
 GEXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr ->
-    let pattern = mk_term k c in
-    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    let pattern = mk_term k c None in
+    if loc_ofCG pattern <> Some !@loc && k = '('
+    then mk_term 'x' c None
+    else pattern ]];
 END
 
 ARGUMENT EXTEND lcpattern
@@ -1043,16 +1071,23 @@ ARGUMENT EXTEND lcpattern
      GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
      RAW_PRINTED BY pr_ssrterm
      GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" lconstr(c) ] -> [ mk_lterm c ]
+| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
 END
 
 GEXTEND Gram
   GLOBAL: lcpattern;
   lcpattern: [[ k = ssrtermkind; c = lconstr ->
-    let pattern = mk_term k c in
-    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    let pattern = mk_term k c None in
+    if loc_ofCG pattern <> Some !@loc && k = '('
+    then mk_term 'x' c None
+    else pattern ]];
 END
 
+let interp_term gl = function
+  | (_, c, Some ist) ->
+      on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
+  | _ -> errorstrm (str"interpreting a term with no ist")
+
 let thin id sigma goal =
   let ids = Id.Set.singleton id in
   let env = Goal.V82.env sigma goal in
@@ -1070,32 +1105,35 @@ let thin id sigma goal =
     let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
     sigma
 
+(*
 let pr_ist { lfun= lfun } =
   prlist_with_sep spc
     (fun (id, Geninterp.Val.Dyn(ty,_)) ->
         pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun)
+*)
 
-let interp_pattern ?wit_ssrpatternarg ist gl red redty =
+let interp_pattern ?wit_ssrpatternarg gl red redty =
   pp(lazy(str"interpreting: " ++ pr_pattern red));
-  pp(lazy(str" in ist: " ++ pr_ist ist));
   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 = k,(x,None) in
-  let decode ist t ?reccall f g =
-    try match DAst.get (pf_intern_term ist gl t) with
+  let mkG ?(k=' ') x ist = k,(x,None), ist in
+  let ist_of (_,_,ist) = ist in
+  let decode (_,_,ist as t) ?reccall f g =
+    try match DAst.get (pf_intern_term gl t) with
     | GCast(t,CastConv c) when isGHole t && isGLambda c->
       let (x, c) = destGLambda c in
-      f x (' ',(c,None))
+      f x (' ',(c,None),ist)
     | GVar id
-      when Id.Map.mem id ist.lfun &&
+      when Option.has_some ist && let ist = Option.get ist in
+           Id.Map.mem id ist.lfun &&
            not(Option.is_empty reccall) &&
            not(Option.is_empty wit_ssrpatternarg) ->
-        let v = Id.Map.find id ist.lfun in
+        let v = Id.Map.find id (Option.get ist).lfun in
         Option.get reccall
           (Value.cast (topwit (Option.get wit_ssrpatternarg)) v)
     | it -> g t with e when CErrors.noncritical e -> g t in
-  let decodeG t f g = decode ist (mkG t) f g in
+  let decodeG ist t f g = decode (mkG t ist) f g in
   let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in
   let cleanup_XinE h x rp sigma =
     let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in
@@ -1128,8 +1166,8 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         thin name sigma e)
       sigma new_evars in
     sigma in
-  let red = let rec decode_red (ist,red) = match red with
-    | T(k,(t,None)) ->
+  let red = let rec decode_red = function
+    | T(k,(t,None),ist) ->
       begin match DAst.get t with
       | GCast (c,CastConv t)
         when isGHole c &&
@@ -1139,48 +1177,51 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         let (id, t) = destGLambda t in
         let id = Id.to_string id in let len = String.length id in
         (match String.sub id 8 (len - 8), DAst.get t with
-        | "In", GApp( _, [t]) -> decodeG t xInT (fun x -> T x)
-        | "In", GApp( _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
+        | "In", GApp( _, [t]) -> decodeG ist t xInT (fun x -> T x)
+        | "In", GApp( _, [e; t]) -> decodeG ist t (eInXInT (mkG e ist)) (bad_enc id)
         | "In", GApp( _, [e; t; e_in_t]) ->
-            decodeG t (eInXInT (mkG e))
-              (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
+            decodeG ist t (eInXInT (mkG e ist))
+              (fun _ -> decodeG ist e_in_t xInT (fun _ -> assert false))
+        | "As", GApp(_, [e; t]) -> decodeG ist t (eAsXInT (mkG e ist)) (bad_enc id)
         | _ -> bad_enc id ())
       | _ ->
-        decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x)
+        decode ~reccall:decode_red (mkG ~k t ist) xInT (fun x -> T x)
       end
-    | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x)
-    | In_T t -> decode ist t inXInT inT
-    | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x)
+    | T t -> decode ~reccall:decode_red t xInT (fun x -> T x)
+    | In_T t -> decode t inXInT inT
+    | X_In_T (e,t) ->  decode t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x)
     | In_X_In_T (e,t) -> inXInT (id_of_Cterm e) t
     | E_In_X_In_T (e,x,rp) -> eInXInT e (id_of_Cterm x) rp
     | E_As_X_In_T (e,x,rp) -> eAsXInT e (id_of_Cterm x) rp in
-    decode_red (ist,red) in
+    decode_red red in
   pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red));
-  let red = match redty with None -> red | Some ty -> let ty = ' ', ty in
+  let red =
+    match redty with
+    | None -> red
+    | Some (ty, ist) -> let ty = ' ', ty, Some ist in
   match red with
   | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
-      let ty = pf_intern_term ist gl ty in
-      E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t)
+      let gty = pf_intern_term gl ty in
+      E_As_X_In_T (mkG (mkRCast mkRHole gty) (ist_of ty), x, t)
   | E_In_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term ist gl ty) in
+      let ty = mkG (pf_intern_term gl ty) (ist_of ty) in
       E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | E_As_X_In_T (e,x,t) ->
-      let ty = mkG (pf_intern_term ist gl ty) in
+      let ty = mkG (pf_intern_term gl ty) (ist_of ty) in
       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)) = match c with
-  | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b))
-  | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
+  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
   match red with
-  | T t -> let sigma, t = interp_term ist gl t in sigma, T t
-  | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
+  | T t -> let sigma, t = interp_term gl t in sigma, T t
+  | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t
   | X_In_T (x, rp) | In_X_In_T (x, rp) ->
     let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in
     let rp = mkXLetIn (Name x) rp in
-    let sigma, rp = interp_term ist gl rp in
+    let sigma, rp = interp_term gl rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
     let rp = subst1 h (nf_evar sigma rp) in
@@ -1189,15 +1230,15 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
     let mk e x p =
       match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in
     let rp = mkXLetIn (Name x) rp in
-    let sigma, rp = interp_term ist gl rp in
+    let sigma, rp = interp_term gl rp in
     let _, h, _, rp = destLetIn rp in
     let sigma = cleanup_XinE h x rp sigma in
     let rp = subst1 h (nf_evar sigma rp) in
-    let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in
+    let sigma, e = interp_term (re_sig (sig_it gl) sigma) e in
     sigma, mk e h rp
 ;;
-let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
-let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;;
+let interp_cpattern gl red redty = interp_pattern gl (T red) redty;;
+let interp_rpattern ~wit_ssrpatternarg gl red = interp_pattern ~wit_ssrpatternarg gl red None;;
 
 let id_of_pattern = function
   | _, T t -> (match kind t with Var id -> Some id | _ -> None)
@@ -1353,25 +1394,20 @@ let pf_fill_occ_term gl occ t =
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
-let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef  id, None), None)
+let cpattern_of_id id =
+  ' ', (DAst.make @@ GRef (VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty })
 
-let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with
+let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
   | _, Some { CAst.v = CHole _ } | GHole _, None -> true
   | _ -> false
 
 (* "ssrpattern" *)
-let pr_ssrpatternarg _ _ _ (_,cpat) = pr_rpattern cpat
-let pr_ssrpatternarg_glob _ _ _ cpat = pr_rpattern cpat
-let interp_ssrpatternarg ist gl p = project gl, (ist, p)
 
-ARGUMENT EXTEND ssrpatternarg
-  PRINTED BY pr_ssrpatternarg
-  INTERPRETED BY interp_ssrpatternarg
-  GLOBALIZED BY glob_rpattern
-  RAW_PRINTED BY pr_ssrpatternarg_glob
-  GLOB_PRINTED BY pr_ssrpatternarg_glob
+ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
 | [ rpattern(pat) ] -> [ pat ]
 END
+
+let pr_rpattern = pr_pattern
   
 let pf_merge_uc uc gl =
   re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc)
@@ -1379,10 +1415,10 @@ let pf_merge_uc uc gl =
 let pf_unsafe_merge_uc uc gl =
   re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc)
 
-let interp_rpattern ist gl red = interp_rpattern ~wit_ssrpatternarg ist gl red
+let interp_rpattern = interp_rpattern ~wit_ssrpatternarg
 
-let ssrpatterntac _ist (arg_ist,arg) gl =
-  let pat = interp_rpattern arg_ist gl arg in
+let ssrpatterntac _ist arg gl =
+  let pat = interp_rpattern gl arg in
   let sigma0 = project gl in
   let concl0 = pf_concl gl in
   let concl0 = EConstr.Unsafe.to_constr concl0 in
@@ -1410,12 +1446,12 @@ let () =
     Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
   Mltop.declare_cache_obj obj "ssrmatching_plugin"
 
-let ssrinstancesof ist arg gl =
+let ssrinstancesof arg gl =
   let ok rhs lhs ise = true in
 (*   not (equal lhs (Evarutil.nf_evar ise rhs)) in *)
   let env, sigma, concl = pf_env gl, project gl, pf_concl gl in
   let concl = EConstr.Unsafe.to_constr concl in
-  let sigma0, cpat = interp_cpattern ist gl arg None in
+  let sigma0, cpat = interp_cpattern gl arg None in
   let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in
   let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in
   let find, conclude =
@@ -1431,7 +1467,7 @@ let ssrinstancesof ist arg gl =
   with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
 
 TACTIC EXTEND ssrinstoftpat
-| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ]
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
 END
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 8ab666f7e..cd5676f28 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -61,7 +61,7 @@ val redex_of_pattern :
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  Tacinterp.interp_sign -> goal sigma ->
+  goal sigma ->
   rpattern ->
     pattern
 
@@ -69,8 +69,8 @@ val interp_rpattern :
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  Tacinterp.interp_sign -> goal sigma ->
-  cpattern -> glob_constr_and_expr option ->
+  goal sigma ->
+  cpattern -> (glob_constr_and_expr * Geninterp.interp_sign) option ->
     pattern
 
 (** The set of occurrences to be matched. The boolean is set to true
@@ -196,7 +196,7 @@ val mk_tpattern_matcher :
 val pf_fill_occ_term : goal sigma -> 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 -> 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