2 files changed, 29 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4809332c5..b17f02f224 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5045,6 +5045,29 @@ let unify ?(state=TransparentState.full) x y =
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
+let with_set_strategy lvl_ql k =
+  let glob_key r =
+    match r with
+    | GlobRef.ConstRef sp -> ConstKey sp
+    | GlobRef.VarRef id -> VarKey id
+    | _ -> user_err Pp.(str
+        "cannot set an inductive type or a constructor as transparent") in
+  let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in
+  Proofview.tclENV >>= fun env ->
+  let orig_kl = List.map (fun (_lvl, k) ->
+      (Conv_oracle.get_strategy (Environ.oracle env) k, k))
+      kl in
+  let env = List.fold_left (fun env (lvl, k) ->
+    Environ.set_oracle env
+      (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
+  Proofview.Unsafe.tclSETENV env <*>
+  k <*>
+  Proofview.tclENV >>= fun env ->
+  let env = List.fold_left (fun env (lvl, k) ->
+    Environ.set_oracle env
+      (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
+  Proofview.Unsafe.tclSETENV env
+
 module Simple = struct
   (** Simplified version of some of the above tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c84ba17f23..fb4367f3aa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -435,6 +435,12 @@ val declare_intro_decomp_eq :
    (types * constr * constr) ->
    constr * types -> unit Proofview.tactic) -> unit
 
+(** Tactic analogous to the [Strategy] vernacular, but only applied
+   locally to the tactic argument *)
+val with_set_strategy :
+  (Conv_oracle.level * Names.GlobRef.t list) list ->
+  unit Proofview.tactic -> unit Proofview.tactic
+
 (** {6 Simple form of basic tactics. } *)
 
 module Simple : sig