Further port of the SSR code.

6 files changed, 23 insertions, 16 deletions

diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 53a5190c99..0674d3d28a 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -97,7 +97,7 @@ let apply_rconstr ?ist t gl =
     if i > n then
       errorstrm Pp.(str"Cannot apply lemma "++pf_pr_glob_constr gl t)
     else try pf_match gl (mkRlemma i) (OfType cl) with _ -> loop (i + 1) in
-  refine_with (loop 0) gl
+  Proofview.V82.of_tactic (refine_with (loop 0)) gl
 
 let mkRAppView ist gl rv gv =
   let nb_view_imps = interp_view_nbimps ist gl rv in
@@ -112,7 +112,7 @@ let refine_interp_apply_view dbl ist gl gv =
     interp_refine ist gl (mkRApp hint (v :: mkRHoles i)) in
   let rec loop = function
   | [] -> (try apply_rconstr ~ist rv gl with _ -> view_error "apply" gv)
-  | h :: hs -> (try refine_with (snd (interp_with h)) gl with _ -> loop hs) in
+  | h :: hs -> (try Proofview.V82.of_tactic (refine_with (snd (interp_with h))) gl with _ -> loop hs) in
   loop (pair dbl (Ssrview.AdaptorDb.get dbl) @
         if dbl = Ssrview.AdaptorDb.Equivalence
         then pair Ssrview.AdaptorDb.Backward (Ssrview.AdaptorDb.(get Backward))
@@ -148,7 +148,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
   | [], [agens] ->
     let clr', (sigma, lemma) = interp_agens ist gl agens in
     let gl = pf_merge_uc_of sigma gl in
-    Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
+    Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [cleartac clr; refine_with ~beta:true lemma; cleartac clr']) gl
   | _, _ ->
      Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
 )
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d643132588..6ab0a16789 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -993,7 +993,8 @@ let dependent_apply_error =
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl =
+let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t =
+  Proofview.V82.tactic begin fun gl ->
   if with_evars then
     let refine gl =
       let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in
@@ -1029,13 +1030,19 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g
          Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t);
          (if first_goes_last then cycle 1 else tclUNIT ())
       ])) gl
+  end
 
-let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
+let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
+  let open Proofview.Notations in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
   let uct = Evd.evar_universe_context (fst oc) in
-  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
-  let gl = pf_unsafe_merge_uc uct gl in
-  try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
-  with e when CErrors.noncritical e -> raise dependent_apply_error
+  let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
+  Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
+  Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+    (fun _ -> Proofview.tclZERO dependent_apply_error)
+  end
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index d6ab326b10..5db55eca91 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -335,7 +335,7 @@ val applyn :
            ?with_shelve:bool ->
            ?first_goes_last:bool ->
            int ->
-           EConstr.t -> v82tac
+           EConstr.t -> unit Proofview.tactic
 exception NotEnoughProducts
 val pf_saturate :
            ?beta:bool ->
@@ -359,7 +359,7 @@ val refine_with :
            ?first_goes_last:bool ->
            ?beta:bool ->
            ?with_evars:bool ->
-           evar_map * EConstr.t -> v82tac
+           evar_map * EConstr.t -> unit Proofview.tactic
 
 val pf_resolve_typeclasses :
   where:EConstr.t ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 8c9dcd9972..b3fa1ea9d0 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -453,7 +453,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
 
   let elim_tac =
     Tacticals.New.tclTHENLIST [
-      Proofview.V82.tactic (refine_with ~with_evars:false elim);
+      refine_with ~with_evars:false elim;
       cleartac clr] in
   let gen_eq_tac = Proofview.V82.tactic gen_eq_tac in
   Tacticals.New.tclTHENLIST [gen_eq_tac; elim_intro_tac ?seed:(Some seed) what eqid elim_tac is_rec clr]
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 7fe673873f..c2ee180855 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -107,7 +107,7 @@ let congrtac ((n, t), ty) ist gl =
       | Some cf -> cf
       | None -> loop (i + 1) in
       loop 1 in
-  tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl
+  Proofview.V82.of_tactic Tacticals.New.(tclTHEN (refine_with cf) (tclTRY Tactics.reflexivity)) gl
 
 let pf_typecheck t gl =
   let it = sig_it gl in
@@ -373,8 +373,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   in
   ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
-  try refine_with
-    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
+  try Proofview.V82.of_tactic (refine_with
+    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl
   with _ ->
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index dcf9c1f7db..708833c52f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -128,7 +128,7 @@ let havetac ist
      let have_let, gl = pf_mkSsrConst "ssr_have_let" gl in
      let step = EConstr.mkApp (have_let, [|concl;t|]) in
      let gl, _ = pf_e_type_of gl step in
-     applyn ~with_evars:true ~with_shelve:false 2 step gl
+     Proofview.V82.of_tactic (applyn ~with_evars:true ~with_shelve:false 2 step) gl
    else basecuttac "ssr_have" t gl in
  (* Introduce now abstract constants, so that everything sees them *)
  let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in