[ssr] get rid of (pf_)mkSsrConst

6 files changed, 55 insertions, 76 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d2e521fb50..06b26b28fd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1240,30 +1240,6 @@ let pfLIFT f =
     Proofview.tclUNIT x
 ;;
 
-(* TASSI: This version of unprotects inlines the unfold tactic definition,
- * since we don't want to wipe out let-ins, and it seems there is no flag
- * to change that behaviour in the standard unfold code *)
-let unprotecttac =
-  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 sigma, c = mkSsrConst "protect_term" env sigma in
-  let prot, _ = EConstr.destConst sigma c in
-  Proofview.Unsafe.tclEVARS sigma <*>
-  Tacticals.New.onClause (fun idopt ->
-    let hyploc = Option.map (fun id -> id, InHyp) idopt in
-    Tactics.reduct_option ~check:false
-      (Reductionops.clos_norm_flags
-        (CClosure.RedFlags.mkflags
-          [CClosure.RedFlags.fBETA;
-           CClosure.RedFlags.fCONST prot;
-           CClosure.RedFlags.fMATCH;
-           CClosure.RedFlags.fFIX;
-           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)
-    allHypsAndConcl
-  end
-
 let is_protect hd env sigma =
   let _, protectC = mkSsrConst "protect_term" env sigma in
   EConstr.eq_constr_nounivs sigma hd protectC
@@ -1521,12 +1497,35 @@ let tclWITHTOP tac = Goal.enter begin fun gl ->
   Tactics.clear [top]
 end
 
-let tacMK_SSR_CONST name = Goal.enter_one ~__LOC__ begin fun g ->
-  let sigma, env = Goal.(sigma g, env g) in
+let tacMK_SSR_CONST name =
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   let sigma, c = mkSsrConst name env sigma in
   Unsafe.tclEVARS sigma <*>
   tclUNIT c
-end
+
+let tacDEST_CONST c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let c, _ = EConstr.destConst sigma c in
+  tclUNIT c
+
+(* TASSI: This version of unprotects inlines the unfold tactic definition,
+ * since we don't want to wipe out let-ins, and it seems there is no flag
+ * to change that behaviour in the standard unfold code *)
+let unprotecttac =
+  tacMK_SSR_CONST "protect_term" >>= tacDEST_CONST >>= fun prot ->
+  Tacticals.New.onClause (fun idopt ->
+    let hyploc = Option.map (fun id -> id, InHyp) idopt in
+    Tactics.reduct_option ~check:false
+      (Reductionops.clos_norm_flags
+        (CClosure.RedFlags.mkflags
+          [CClosure.RedFlags.fBETA;
+           CClosure.RedFlags.fCONST prot;
+           CClosure.RedFlags.fMATCH;
+           CClosure.RedFlags.fFIX;
+           CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)
+    allHypsAndConcl
+
 
 module type StateType = sig
   type state
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index e1c3b051d7..d1ad24496e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -233,15 +233,8 @@ val pf_abs_prod :
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 
 val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
-val mkSsrConst :
-           string ->
-           env -> evar_map -> evar_map * EConstr.t
-val pf_mkSsrConst :
-           string ->
-           Goal.goal Evd.sigma ->
-           EConstr.t * Goal.goal Evd.sigma
-val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 
+val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx
 
 val pf_fresh_global :
            GlobRef.t ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 6bfd500b3c..ab07dd5be9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -120,6 +120,9 @@ let pf_typecheck t gl =
   re_sig [it] sigma
 
 let newssrcongrtac arg ist =
+  let open Proofview.Notations in
+  Proofview.Goal.enter_one ~__LOC__ begin fun _g ->
+    (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr ->
   Proofview.V82.tactic begin fun gl ->
   ppdebug(lazy Pp.(str"===newcongr==="));
   ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
@@ -137,7 +140,6 @@ let newssrcongrtac arg ist =
     let sigma = Evd.create_evar_defs sigma in
     let (sigma, x) = Evarutil.new_evar env sigma ty in
     x, re_sig si sigma in
-  let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
   let ssr_congr lr = EConstr.mkApp (arr, lr) in
   let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
   (* here the two cases: simple equality or arrow *)
@@ -720,9 +722,6 @@ let unfoldtac occ ko t kt =
 
 let unlocktac ist args =
   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 utac (occ, gt) =
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
@@ -730,12 +729,10 @@ let unlocktac ist args =
       unfoldtac occ occ (interp_term env sigma ist gt) (fst gt)
     end
   in
-  let sigma, locked = mkSsrConst "locked" env sigma in
-  let sigma, key = mkSsrConst "master_key" env sigma in
+  Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked ->
+  Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key ->
   let ktacs = [
     (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens);
     Ssrelim.casetac key (fun ?seed:_ k -> k)
   ] in
-  Proofview.Unsafe.tclEVARS sigma <*>
   Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
-  end
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index d319eba8aa..4961138190 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -89,17 +89,19 @@ let combineCG t1 t2 f g = match t1, t2 with
  | _, (_, (_, None)) -> anomaly "have: mixed C-G constr"
  | _ -> anomaly "have: mixed G-C constr"
 
-let basecuttac name c =
+let basecuttac name t =
   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 sigma, hd = mkSsrConst name env sigma in
-  let t = EConstr.mkApp (hd, [|c|]) in
-  let sigma, _ = Typing.type_of env sigma t in
-  Proofview.Unsafe.tclEVARS sigma <*>
+  Ssrcommon.tacMK_SSR_CONST name >>= fun hd ->
+  let t = EConstr.mkApp (hd, [|t|]) in
+  Ssrcommon.tacTYPEOF t >>= fun _ty ->
   Tactics.apply t
-  end
+
+let evarcuttac name cs =
+  let open Proofview.Notations in
+  Ssrcommon.tacMK_SSR_CONST name >>= fun hd ->
+  let t = EConstr.mkApp (hd, cs) in
+  Ssrcommon.tacTYPEOF t >>= fun _ty ->
+  applyn ~with_evars:true ~with_shelve:false (Array.length cs) t
 
 let introstac ipats = tclIPAT ipats
 
@@ -107,6 +109,9 @@ let havetac ist
   (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint)))
   suff namefst
 =
+ let open Proofview.Notations in
+ Ssrcommon.tacMK_SSR_CONST "abstract_key" >>= fun abstract_key ->
+ Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
  Proofview.V82.tactic begin fun gl ->
  let concl = pf_concl gl in
  let pats = tclCompileIPats orig_pats in
@@ -129,21 +134,11 @@ let havetac ist
    not !ssrhaveNOtcresolution &&
    match fk with FwdHint(_,true) -> false | _ -> true in
  let hint = hinttac ist true hint in
- let cuttac t =
-  let open Proofview.Notations in
-  Proofview.Goal.enter begin fun gl ->
-   if transp then
-    let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
-     let sigma, have_let = mkSsrConst "ssr_have_let" env sigma in
-     let step = EConstr.mkApp (have_let, [|concl;t|]) in
-     let sigma, _ = Typing.type_of env sigma step in
-     Proofview.Unsafe.tclEVARS sigma <*>
-     applyn ~with_evars:true ~with_shelve:false 2 step
+ let cuttac t = Proofview.Goal.enter begin fun gl ->
+   if transp then evarcuttac "ssr_have_let" [|concl;t|]
    else basecuttac "ssr_have" t
   end in
  (* Introduce now abstract constants, so that everything sees them *)
- let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
  let unlock_abs (idty,args_id) gl =
     let gl, _ = pf_e_type_of gl idty in
     pf_unify_HO gl args_id.(2) abstract_key in
@@ -203,7 +198,6 @@ let havetac ist
      gl, ty, Tactics.apply t, id,
        Tacticals.New.tclTHEN (Tacticals.New.tclTHEN itac_c simpltac)
          (Tacticals.New.tclTHEN tacopen_skols (Proofview.V82.tactic (fun gl ->
-            let abstract, gl = pf_mkSsrConst "abstract" gl in
             Proofview.V82.of_tactic (unfold [abstract; abstract_key]) gl)))
    | _,true,true  ->
      let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in
@@ -361,16 +355,14 @@ let intro_lock ipats =
              Proofview.tclDISPATCH
                (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
   let protect_subgoal env sigma hd args =
+    Ssrcommon.tacMK_SSR_CONST "Under_rel" >>= fun under_rel ->
+    Ssrcommon.tacMK_SSR_CONST "Under_rel_from_rel" >>= fun under_from_rel ->
     Tactics.New.refine ~typecheck:true (fun sigma ->
         let lm2 = Array.length args - 2 in
         let sigma, carrier =
           Typing.type_of env sigma args.(lm2) in
         let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in
         let rel_args = Array.sub args lm2 2 in
-        let sigma, under_rel =
-          Ssrcommon.mkSsrConst "Under_rel" env sigma in
-        let sigma, under_from_rel =
-          Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in
         let under_rel_args = Array.append [|carrier; rel|] rel_args in
         let ty = EConstr.mkApp (under_rel, under_rel_args) in
         let sigma, t = Evarutil.new_evar env sigma ty in
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index dc90b159d7..33bf56cfa9 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -29,9 +29,7 @@ val havetac : ist ->
            bool ->
            bool -> unit Proofview.tactic
 
-val basecuttac :
-           string ->
-           EConstr.t -> unit Proofview.tactic
+val basecuttac : string -> EConstr.t -> unit Proofview.tactic
 
 val wlogtac :
   Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index c102111e52..46f90a7ee1 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -384,13 +384,11 @@ end
 
 let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
   let env, concl = Goal.(env gl, concl gl) in
-  let step = begin fun sigma ->
+  let step ablock abstract = begin fun sigma ->
     let (sigma, (abstract_proof, abstract_ty)) =
       let (sigma, (ty, _)) =
         Evarutil.new_type_evar env sigma Evd.univ_flexible_alg in
-      let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
       let (sigma, lock) = Evarutil.new_evar env sigma ablock in
-      let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
       let (sigma, abstract_id) = mk_abstract_id env sigma in
       let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
       let sigma, m = Evarutil.new_evar env sigma abstract_ty in
@@ -405,7 +403,9 @@ let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
     let sigma, _ = Typing.type_of env sigma term in
     sigma, term
   end in
-  Tactics.New.refine ~typecheck:false step <*>
+  Ssrcommon.tacMK_SSR_CONST "abstract_lock" >>= fun ablock ->
+  Ssrcommon.tacMK_SSR_CONST "abstract" >>= fun abstract ->
+  Tactics.New.refine ~typecheck:false (step ablock abstract) <*>
   tclFOCUS 1 3 Proofview.shelve
 end