Remove legacy SSR API.

6 files changed, 18 insertions, 16 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 32a215444b..42b9248979 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -58,7 +58,7 @@ let interp_nbargs ist gl rc =
     let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc6, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    6 + Ssrcommon.nbargs_open_constr gl t
+    6 + Ssrcommon.nbargs_open_constr (pf_env gl) t
   with _ -> 5
 
 let interp_view_nbimps ist gl rc =
@@ -66,7 +66,7 @@ let interp_view_nbimps ist gl rc =
     let sigma, t = interp_open_constr (pf_env gl) (project gl) ist (rc, None) in
     let si = sig_it gl in
     let gl = re_sig si sigma in
-    let pl, c = splay_open_constr gl t in
+    let pl, c = splay_open_constr (pf_env gl) t in
     if Ssrcommon.isAppInd (pf_env gl) (project gl) c then List.length pl else (-(List.length pl))
   with _ -> 0
 
@@ -88,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
   let n = match ist, DAst.get t with
-    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
+    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs (pf_env gl) (project gl) (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e0a1cbce3a..64c4914054 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -221,8 +221,8 @@ let intern_term ist env (_, c) = glob_constr ist env c
 (* FUNCLASS, which is probably just as well since these can     *)
 (* lead to infinite arities.                                    *)
 
-let splay_open_constr gl (sigma, c) =
-  let env = pf_env gl in let t = Retyping.get_type_of env sigma c in
+let splay_open_constr env (sigma, c) =
+  let t = Retyping.get_type_of env sigma c in
   Reductionops.splay_prod env sigma t
 
 let isAppInd env sigma c =
@@ -322,10 +322,10 @@ let ssrdgens_of_parsed_dgens = function
   | _ -> assert false
 
 
-let nbargs_open_constr gl oc =
-  let pl, _ = splay_open_constr gl oc in List.length pl
+let nbargs_open_constr env oc =
+  let pl, _ = splay_open_constr env oc in List.length pl
 
-let pf_nbargs gl c = nbargs_open_constr gl (project gl, c)
+let pf_nbargs env sigma c = nbargs_open_constr env (sigma, c)
 
 let internal_names = ref []
 let add_internal_name pt = internal_names := pt :: !internal_names
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 362e488d8a..00b2e56221 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -155,7 +155,7 @@ val pf_e_type_of :
   EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
 
 val splay_open_constr :
-           Goal.goal Evd.sigma ->
+           Environ.env ->
            evar_map * EConstr.t ->
            (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
 val isAppInd : Environ.env -> Evd.evar_map -> EConstr.types -> bool
@@ -262,8 +262,8 @@ val abs_evars_pirrel :
 val pf_abs_evars_pirrel :
            Goal.goal Evd.sigma ->
            evar_map * Constr.constr -> int * Constr.constr
-val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int
-val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int
+val nbargs_open_constr : Environ.env -> Evd.evar_map * EConstr.t -> int
+val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int
 val gen_tmp_ids :
            ?ist:Geninterp.interp_sign ->
            (Goal.goal * tac_ctx) Evd.sigma ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index d52b83d529..6036642fbd 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -95,7 +95,7 @@ let congrtac ((n, t), ty) ist gl =
   let ist' = {ist with lfun =
     Id.Map.add pattern_id (Tacinterp.Value.of_constr f) Id.Map.empty } in
   let rf = mkRltacVar pattern_id in
-  let m = pf_nbargs gl f in
+  let m = pf_nbargs (pf_env gl) (project gl) f in
   let _, cf = if n > 0 then
     match interp_congrarg_at ist' gl n rf ty m with
     | Some cf -> cf
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 30957bbc79..adaf7c8cc1 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1224,23 +1224,23 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
  let rdx, _, (sigma, uc, p) = end_U () in
  sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx
 
-let fill_occ_term env cl occ sigma0 (sigma, t) =
+let fill_occ_term env sigma0 cl occ (sigma, t) =
   try
     let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in
     if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars")
-    else cl, (Evd.merge_universe_context sigma' uc, t')
+    else cl, t'
   with NoMatch -> try
     let sigma', uc, t' =
       unif_end env sigma0 (create_evar_defs sigma) t (fun _ -> true) in
     if sigma' != sigma0 then raise NoMatch
-    else cl, (Evd.merge_universe_context sigma' uc, t')
+    else cl, t'
   with _ ->
     errorstrm (str "partial term " ++ pr_econstr_pat env sigma t
             ++ str " does not match any subterm of the goal")
 
 let pf_fill_occ_term gl occ t =
   let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
-  let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
+  let cl, t = fill_occ_term env sigma0 concl occ t in
   cl, t
 
 let cpattern_of_id id =
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 4a30544a74..17b47227cb 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -191,6 +191,8 @@ val mk_tpattern_matcher :
  * by [Rel 1] and the instance of [t] *)
 val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> 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