Remove legacy layer in SSR.

7 files changed, 45 insertions, 60 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 29f52d8834..e0a1cbce3a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1144,7 +1144,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr)
 
 (* XXX the k of the redex should percolate out *)
 let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
-  let pat = interp_cpattern gl t None in (* UGLY API *)
+  let pat = interp_cpattern (pf_env gl) (project gl) t None in (* UGLY API *)
   let gl = pf_merge_uc_of (fst pat) gl in
   let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in
   let (c, ucst), cl =
@@ -1287,7 +1287,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
      gl, EConstr.mkVar x :: args, prod
   | _, Some ((x, "@"), Some p) ->
      let x = hoi_id x in
-     let cp = interp_cpattern gl p None in
+     let cp = interp_cpattern (pf_env gl) (project gl) p None in
      let gl = pf_merge_uc_of (fst cp) gl in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
@@ -1300,7 +1300,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
      pf_merge_uc ucst gl, args, EConstr.mkLetIn(make_annot (Name (f x)) r, ut, ty, c)
   | _, Some ((x, _), Some p) ->
      let x = hoi_id x in
-     let cp = interp_cpattern gl p None in
+     let cp = interp_cpattern (pf_env gl) (project gl) p None in
      let gl = pf_merge_uc_of (fst cp) gl in
      let (t, ucst), c =
        try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1
@@ -1489,7 +1489,7 @@ end
 
 let tacINTERP_CPATTERN cp =
   tacSIGMA >>= begin fun gl ->
-  tclUNIT (Ssrmatching.interp_cpattern gl cp None)
+  tclUNIT (Ssrmatching.interp_cpattern (pf_env gl) (project gl) cp None)
 end
 
 let tacUNIFY a b =
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 6155f8fbf6..60ffe6ceb6 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -183,7 +183,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         else
           let c = Option.get oc in let gl, c_ty = pfe_type_of gl c in
           let pc = match c_gen with
-            | Some p -> interp_cpattern orig_gl p None
+            | Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None
             | _ -> mkTpat gl c in
           Some(c, c_ty, pc), gl in
       seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
@@ -233,7 +233,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
         pf_saturate ~beta:is_case gl elim ~ty:elimty n_elim_args in
       let pred = List.assoc pred_id elim_args in
       let pc = match n_c_args, c_gen with
-        | 0, Some p -> interp_cpattern orig_gl p None
+        | 0, Some p -> interp_cpattern (pf_env orig_gl) (project orig_gl) p None
         | _ -> mkTpat gl c in
       let cty = Some (c, c_ty, pc) in
       let elimty = Reductionops.whd_all env (project gl) elimty in
@@ -312,7 +312,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
       | ((oclr, occ), t):: deps, inf_t :: inf_deps ->
-          let p = interp_cpattern orig_gl t None in
+          let p = interp_cpattern (pf_env orig_gl) (project orig_gl) t None in
           let clr_t =
             interp_clr (project gl) (oclr,(tag_of_cpattern t,EConstr.of_constr (fst (redex_of_pattern env p)))) in
           (* if we are the index for the equation we do not clear *)
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1e3e2e69ea..1e4faa3eee 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -637,7 +637,7 @@ end
 let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
   let interp_rpattern gl gc =
-    try interp_rpattern gl gc
+    try interp_rpattern (pf_env gl) (project gl) gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
   let interp gc gl =
     try interp_term (pf_env gl) (project gl) ist gc
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index b2e6f69e95..6ff59f21a3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -43,7 +43,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) =
   let pty = Option.map (fun { Ssrast.body; interp_env } ->
     let ist = Option.get interp_env in
     (mkRHole, Some body), ist) pty in
-  let pat = interp_cpattern gl pat pty in
+  let pat = interp_cpattern (pf_env gl) (project gl) pat pty in
   let cl, sigma, env = pf_concl gl, project gl, pf_env gl in
   let (c, ucst), cl =
     let cl = EConstr.Unsafe.to_constr cl in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 16fd5235a2..c102111e52 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -727,7 +727,7 @@ let mkEq dir cl c t n env sigma =
 let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
   Ssrcommon.tacSIGMA >>= fun sigma0 ->
   Goal.enter_one begin fun g ->
-  let pat = Ssrmatching.interp_cpattern sigma0 t None in
+  let pat = Ssrmatching.interp_cpattern (Tacmach.pf_env sigma0) (Tacmach.project sigma0) t None in
   let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
   let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in
   let (c, ucst), cl =
@@ -985,7 +985,7 @@ let ssrabstract dgens =
    Ssrcommon.tacSIGMA >>= fun gl0 ->
      let open Ssrmatching in
      let ipats = List.map (fun (_,cp) ->
-       match id_of_pattern (interp_cpattern gl0 cp None) with
+       match id_of_pattern (interp_cpattern (Tacmach.pf_env gl0) (Tacmach.project gl0) cp None) with
        | None -> IPatAnon (One None)
        | Some id -> IPatId id)
        (List.tl gens) in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6a36959e83..cc2345c7f8 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -14,7 +14,6 @@ open Ltac_plugin
 open Names
 open Pp
 open Genarg
-open Stdarg
 open Term
 open Context
 module CoqConstr = Constr
@@ -173,8 +172,6 @@ let loc_ofCG = function
 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
-
 let nf_evar sigma c =
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
 
@@ -932,31 +929,15 @@ let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
   | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
 
-let of_ftactic ftac gl =
-  let r = ref None in
-  let tac = Ftactic.run ftac (fun ans -> r := Some ans; Proofview.tclUNIT ()) in
-  let tac = Proofview.V82.of_tactic tac in
-  let { sigma = sigma } = tac gl in
-  let ans = match !r with
-  | None -> assert false (* If the tactic failed we should not reach this point *)
-  | Some ans -> ans
-  in
-  (sigma, ans)
-
-let interp_wit wit ist gl x =
-  let globarg = in_gen (glbwit wit) x in
-  let arg = interp_genarg ist globarg in
-  let (sigma, arg) = of_ftactic arg gl in
-  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 gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c
+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 interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
 
-let interp_term gl = function
+let interp_term env sigma = function
   | (_, c, Some ist) ->
-      on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
+      on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c)
   | _ -> errorstrm (str"interpreting a term with no ist")
 
 let thin id sigma goal =
@@ -982,7 +963,7 @@ let pr_ist { lfun= lfun } =
         pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun)
 *)
 
-let interp_pattern ?wit_ssrpatternarg gl red redty =
+let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
   pp(lazy(str"interpreting: " ++ pr_pattern 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
@@ -990,7 +971,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   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
+    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)
@@ -1008,7 +989,7 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   let cleanup_XinE h x rp sigma =
     let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in
     let to_clean, update = (* handle rename if x is already used *)
-      let ctx = pf_hyps gl in
+      let ctx = Environ.named_context env in
       let len = Context.Named.length ctx in
       let name = ref None in
       try ignore(Context.Named.lookup x ctx); (name, fun k ->
@@ -1019,7 +1000,6 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
           name := Some (Context.Named.Declaration.get_id (List.nth nctx (nlen - len - 1)))
         end)
       with Not_found -> ref (Some x), fun _ -> () in
-    let sigma0 = project gl in
     let new_evars =
       let rec aux acc t = match kind t with
       | Evar (k,_) ->
@@ -1072,13 +1052,13 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   match red with
   | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
-      let gty = pf_intern_term gl ty in
+      let gty = pf_intern_term env sigma0 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 gl ty) (ist_of ty) in
+      let ty = mkG (pf_intern_term env sigma0 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 gl ty) (ist_of ty) in
+      let ty = mkG (pf_intern_term env sigma0 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));
@@ -1086,12 +1066,12 @@ let interp_pattern ?wit_ssrpatternarg gl red redty =
   | 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 gl t in sigma, T t
-  | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t
+  | 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
   | 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 gl rp in
+    let sigma, rp = interp_term env sigma0 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
@@ -1100,15 +1080,15 @@ let interp_pattern ?wit_ssrpatternarg 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 gl rp in
+    let sigma, rp = interp_term env sigma0 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 (re_sig (sig_it gl) sigma) e in
+    let sigma, e = interp_term env sigma e in
     sigma, mk e h rp
 ;;
-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 interp_cpattern env sigma red redty = interp_pattern env sigma (T red) redty;;
+let interp_rpattern ~wit_ssrpatternarg env sigma red = interp_pattern ~wit_ssrpatternarg env sigma red None;;
 
 let id_of_pattern = function
   | _, T t -> (match kind t with Var id -> Some id | _ -> None)
@@ -1286,18 +1266,23 @@ let wit_ssrpatternarg = wit_rpatternty
 
 let interp_rpattern = interp_rpattern ~wit_ssrpatternarg
 
-let ssrpatterntac _ist arg gl =
-  let pat = interp_rpattern gl arg in
-  let sigma0 = project gl in
-  let concl0 = pf_concl gl in
+let ssrpatterntac _ist arg =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma0 = Proofview.Goal.sigma gl in
+  let concl0 = Proofview.Goal.concl gl in
+  let env = Proofview.Goal.env gl in
+  let pat = interp_rpattern env sigma0 arg in
   let concl0 = EConstr.Unsafe.to_constr concl0 in
   let (t, uc), concl_x =
-    fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in
+    fill_occ_pattern env sigma0 concl0 pat noindex 1 in
   let t = EConstr.of_constr t in
   let concl_x = EConstr.of_constr concl_x in
-  let gl, tty = pf_type_of gl t in
+  let sigma, tty = Typing.type_of env sigma0 t in
   let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in
-  Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl
+  Proofview.Unsafe.tclEVARS sigma <*>
+  convert_concl ~check:true concl DEFAULTcast
+  end
 
 (* Register "ssrpattern" tactic *)
 let () =
@@ -1305,7 +1290,7 @@ let () =
     let arg =
       let v = Id.Map.find (Names.Id.of_string "pattern") ist.lfun in
       Value.cast (topwit wit_ssrpatternarg) v in
-    Proofview.V82.tactic (ssrpatterntac ist arg) in
+    ssrpatterntac ist arg in
   let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in
   let () = Tacenv.register_ml_tactic name [|mltac|] in
   let tac =
@@ -1321,7 +1306,7 @@ let ssrinstancesof arg =
 (*   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 gl arg None in
+  let sigma0, cpat = interp_cpattern (pf_env gl) (project 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 =
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 176dfa92b2..4a30544a74 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -57,7 +57,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 :
-  goal sigma ->
+  Environ.env -> Evd.evar_map ->
   rpattern ->
     pattern
 
@@ -65,7 +65,7 @@ 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 :
-  goal sigma ->
+  Environ.env -> Evd.evar_map ->
   cpattern -> (glob_constr_and_expr * Geninterp.interp_sign) option ->
     pattern