Export a function to apply toplevel tactic values in Tacinterp.

This is a function that keeps beeing asked or reimplemented. It doesn't hurt
adding it to the Ltac API.

3 files changed, 28 insertions, 27 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d89..6d94e3f86 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -141,16 +141,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with
 | None -> []
 | Some l -> l
 
-module Value = struct
-
-  include Taccoerce.Value
-
-  let of_closure ist tac =
-    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    of_tacvalue closure
-
-end
-
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
 let catching_error call_trace fail (e, info) =
@@ -1860,6 +1850,31 @@ let eval_tactic_ist ist t =
   Proofview.tclLIFT db_initialize <*>
   interp_tactic ist t
 
+(** FFI *)
+
+module Value = struct
+
+  include Taccoerce.Value
+
+  let of_closure ist tac =
+    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+    of_tacvalue closure
+
+  (** Apply toplevel tactic values *)
+  let apply (f : value) (args: value list) =
+    let fold arg (i, vars, lfun) =
+      let id = Id.of_string ("x" ^ string_of_int i) in
+      let x = Reference (ArgVar CAst.(make id)) in
+      (succ i, x :: vars, Id.Map.add id arg lfun)
+    in
+    let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+    let lfun = Id.Map.add (Id.of_string "F") f lfun in
+    let ist = { (default_ist ()) with lfun = lfun; } in
+    let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    eval_tactic_ist ist tac
+
+end
+
 (* globalization + interpretation *)
 
 
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fd2d96bd6..f9883e444 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -28,6 +28,7 @@ sig
   val to_list : t -> t list option
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
   val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
+  val apply : t -> t list -> unit Proofview.tactic
 end
 
 (** Values for interpretation *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 8e0ca877a..a736eec5e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -161,21 +161,6 @@ let decl_constant na univs c =
 let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
 
-(* Calling a locally bound tactic *)
-let ltac_lcall tac args =
-  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
-
-let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
-  let fold arg (i, vars, lfun) =
-    let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar CAst.(make id)) in
-    (succ i, x :: vars, Id.Map.add id arg lfun)
-  in
-  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
-  let lfun = Id.Map.add (Id.of_string "F") f lfun in
-  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
-  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
-
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
     Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
@@ -765,7 +750,7 @@ let ring_lookup (f : Value.t) lH rl t =
       let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let ring = ltac_ring_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
@@ -1051,6 +1036,6 @@ let field_lookup (f : Value.t) lH rl t =
       let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let field = ltac_field_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
+      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end