Further porting of ssrcode.

5 files changed, 30 insertions, 27 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 692b13c2bb..53a5190c99 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -55,7 +55,7 @@ let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
 let interp_nbargs ist gl rc =
   try
     let rc6 = mkRApp rc (mkRHoles 6) in
-    let sigma, t = interp_open_constr ist gl (rc6, None) in
+    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
@@ -63,7 +63,7 @@ let interp_nbargs ist gl rc =
 
 let interp_view_nbimps ist gl rc =
   try
-    let sigma, t = interp_open_constr ist gl (rc, None) in
+    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
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index bcdcd0af4a..6cbb92163e 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -253,11 +253,11 @@ let interp_refine ist gl rc =
   (sigma, (sigma, c))
 
 
-let interp_open_constr ist gl gc =
-  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
-  (project gl, (sigma, c))
+let interp_open_constr env sigma0 ist gc =
+  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist env sigma0 (gc, Tactypes.NoBindings) in
+  (sigma0, (sigma, c))
 
-let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
+let interp_term env sigma ist (_, c) = snd (interp_open_constr env sigma ist c)
 
 let of_ftactic ftac gl =
   let r = ref None in
@@ -845,7 +845,7 @@ let rewritetac ?(under=false) dir c =
 type name_hint = (int * EConstr.types array) option ref
 
 let pf_abs_ssrterm ?(resolve_typeclasses=false) ist gl t =
-  let sigma, ct as t = interp_term ist gl t in
+  let sigma, ct as t = interp_term (pf_env gl) (project gl) ist t in
   let sigma, _ as t =
     let env = pf_env gl in
     if not resolve_typeclasses then t
@@ -917,7 +917,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
      | LetInType(n,v,ty,t) -> decr n_binders; mkLetIn (n, v, ty, aux t)
      | _ -> anomaly "pf_interp_ty: ssr Type cast deleted by typecheck" in
      sigma, aux t in
-   let sigma, cty as ty = strip_cast (interp_term ist gl ty) in
+   let sigma, cty as ty = strip_cast (interp_term (pf_env gl) (project gl) ist ty) in
    let ty =
      let env = pf_env gl in
      if not resolve_typeclasses then ty
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index f655457c63..a8b95c39ff 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -131,7 +131,8 @@ val pf_intern_term :
     ssrterm -> Glob_term.glob_constr
 
 val interp_term :
-  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
+  Environ.env -> Evd.evar_map ->
+  Tacinterp.interp_sign ->
     ssrterm -> evar_map * EConstr.t
 
 val interp_wit :
@@ -145,7 +146,8 @@ val interp_refine :
     Glob_term.glob_constr -> evar_map * (evar_map * EConstr.constr)
 
 val interp_open_constr :
-  Tacinterp.interp_sign -> Goal.goal Evd.sigma ->
+  Environ.env -> Evd.evar_map ->
+  Tacinterp.interp_sign ->
     Genintern.glob_constr_and_expr -> evar_map * (evar_map * EConstr.t)
 
 val pf_e_type_of :
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 33a2eb85d9..7fe673873f 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -89,7 +89,7 @@ let pattern_id = mk_internal_id "pattern value"
 let congrtac ((n, t), ty) ist gl =
   ppdebug(lazy (Pp.str"===congr==="));
   ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
-  let sigma, _ as it = interp_term ist gl t in
+  let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in
   let gl = pf_merge_uc_of sigma gl in
   let _, f, _, _ucst = pf_abs_evars gl it in
   let ist' = {ist with lfun =
@@ -484,8 +484,7 @@ let closed0_check cl p gl =
 
 let dir_org = function L2R -> 1 | R2L -> 2
 
-let rwprocess_rule dir rule gl =
-  let env = pf_env gl in
+let rwprocess_rule env dir rule =
   let coq_prod = lz_coq_prod () in
   let is_setoid = ssr_is_setoid env in
   let r_sigma, rules =
@@ -564,7 +563,7 @@ let rwprocess_rule dir rule gl =
 
 let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
   let env = pf_env gl in
-  let r_sigma, rules = rwprocess_rule dir rule gl in
+  let r_sigma, rules = rwprocess_rule env dir rule in
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
@@ -604,10 +603,12 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
 ;;
 
 let ssrinstancesofrule ist dir arg =
-  Proofview.V82.tactic begin fun gl ->
-  let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in
-  let rule = interp_term ist gl arg in
-  let r_sigma, rules = rwprocess_rule dir rule gl in
+  Proofview.Goal.enter begin fun gl ->
+  let env0 = Proofview.Goal.env gl in
+  let sigma0 = Proofview.Goal.sigma gl in
+  let concl0 = Proofview.Goal.concl gl in
+  let rule = interp_term env0 sigma0 ist arg in
+  let r_sigma, rules = rwprocess_rule env0 dir rule in
   let find, conclude =
     let upats_origin = dir, EConstr.Unsafe.to_constr (snd rule) in
     let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
@@ -624,9 +625,9 @@ let ssrinstancesofrule ist dir arg =
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
-      ignore(find env0 (EConstr.Unsafe.to_constr concl0) 1 ~k:print)
+      ignore(find env0 (EConstr.to_constr sigma0 concl0) 1 ~k:print)
     done; raise NoMatch
-  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
+  with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); Tacticals.New.tclIDTAC
   end
 
 let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl ->
@@ -639,7 +640,7 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt)
     try interp_rpattern gl gc
     with _ when snd mult = May -> fail := true; project gl, T mkProp in
   let interp gc gl =
-    try interp_term ist gl gc
+    try interp_term (pf_env gl) (project gl) ist gc
     with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in
   let rwtac gl =
     let rx = Option.map (interp_rpattern gl) grx in
@@ -679,7 +680,7 @@ let unfoldtac occ ko t kt gl =
 let unlocktac ist args =
   Proofview.V82.tactic begin fun gl ->
   let utac (occ, gt) gl =
-    unfoldtac occ occ (interp_term ist gl gt) (fst gt) gl in
+    unfoldtac occ occ (interp_term (pf_env gl) (project gl) ist gt) (fst gt) gl in
   let locked, gl = pf_mkSsrConst "locked" gl in
   let key, gl = pf_mkSsrConst "master_key" gl in
   let ktacs = [
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 6d3c5d8807..4f9747ae73 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -151,15 +151,15 @@ let tclCLAUSES tac (gens, clseq) =
 (** The "do" tactical. ********************************************************)
 
 let hinttac ist is_by (is_or, atacs) =
-  Proofview.V82.tactic begin
-  let dtac = if is_by then Proofview.V82.of_tactic (donetac ~-1) else Tacticals.tclIDTAC in
+  Proofview.Goal.enter begin fun _ ->
+  let dtac = if is_by then donetac ~-1 else Tacticals.New.tclIDTAC in
   let mktac = function
-  | Some atac -> Tacticals.tclTHEN (Proofview.V82.of_tactic (ssrevaltac ist atac)) dtac
+  | Some atac -> Tacticals.New.tclTHEN (ssrevaltac ist atac) dtac
   | _ -> dtac in
   match List.map mktac atacs with
-  | [] -> if is_or then dtac else Tacticals.tclIDTAC
+  | [] -> if is_or then dtac else Tacticals.New.tclIDTAC
   | [tac] -> tac
-  | tacs -> Tacticals.tclFIRST tacs
+  | tacs -> Tacticals.New.tclFIRST tacs
   end
 
 let ssrdotac ist (((n, m), tac), clauses) =