The tactic generic argument now returns a value rather than a glob_expr.

The glob_expr was actually always embedded as a VFun, so this patch should
not change anything semantically. The only change occurs in the plugin API
where one should use the Tacinterp.tactic_of_value function instead of
Tacinterp.eval_tactic.

Moreover, this patch allows to use tactics returning arguments from the ML
side.

6 files changed, 18 insertions, 18 deletions

diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7c206d95cb..7df845e4bd 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -47,7 +47,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val wit_by_arg_tac :
   (raw_tactic_expr option,
   glob_tactic_expr option,
-  glob_tactic_expr option) Genarg.genarg_type
+  Genarg.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cdf29e4c62..151949c3c6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -44,7 +44,7 @@ let with_delayed_uconstr ist c tac =
 
 let replace_in_clause_maybe_by ist c1 c2 cl tac =
   with_delayed_uconstr ist c1
-  (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
+  (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
 
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
@@ -237,7 +237,7 @@ TACTIC EXTEND autorewrite
     [ auto_multi_rewrite  l ( cl) ]
 | [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
     [
-      auto_multi_rewrite_with (Tacinterp.eval_tactic t) l cl
+      auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
     ]
 END
 
@@ -245,14 +245,14 @@ TACTIC EXTEND autorewrite_star
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
     [ auto_multi_rewrite ~conds:AllMatches l cl ]
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
-  [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.eval_tactic t) l cl ]
+  [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ]
 END
 
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
-let rewrite_star ist clause orient occs c (tac : glob_tactic_expr option) =
-  let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
+let rewrite_star ist clause orient occs c (tac : Val.t option) =
+  let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
   with_delayed_uconstr ist c
     (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
 
@@ -512,12 +512,12 @@ let add_transitivity_lemma left lem =
 (* Vernacular syntax *)
 
 TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.eval_tactic tac) ]
+| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ]
 | ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ]
 END
 
 TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.eval_tactic tac) ]
+| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ]
 | ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ]
 END
 
@@ -883,7 +883,7 @@ END
 TACTIC EXTEND unshelve
 | [ "unshelve" tactic1(t) ] ->
     [
-      Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
+      Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
       Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
       Proofview.Unsafe.tclSETGOALS (gls @ ogls)
     ]
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index e0c1f671fd..766593543c 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -14,7 +14,7 @@ open Class_tactics
 DECLARE PLUGIN "g_class"
 
 TACTIC EXTEND progress_evars
-  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ]
+  [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ]
 END
 
 (** Options: depth, debug and transparency settings. *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2af21fac6e..cb4a9f320d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1458,7 +1458,7 @@ and tactic_of_value ist vle =
   | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
-    eval_tactic ist tac
+    tactic_of_value ist tac
   else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
@@ -2232,10 +2232,7 @@ let () =
   ()
 
 let () =
-  let interp ist tac =
-    let f = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    Ftactic.return (TacArg (dloc, TacGeneric (Genarg.in_gen (glbwit wit_tacvalue) f)))
-  in
+  let interp ist tac = Ftactic.return (Value.of_closure ist tac) in
   Geninterp.register_interp0 wit_tactic interp
 
 let () =
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 89d34231b8..c5da3494cb 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -88,6 +88,8 @@ val eval_tactic : glob_tactic_expr -> unit Proofview.tactic
 val eval_tactic_ist : interp_sign -> glob_tactic_expr -> unit Proofview.tactic
 (** Same as [eval_tactic], but with the provided [interp_sign]. *)
 
+val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
+
 (** Globalization + interpretation *)
 
 val interp_tac_gen : value Id.Map.t -> Id.t list ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4dc5388eeb..5485f344b3 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -352,7 +352,6 @@ let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff"
 
 let intuition_gen ist flags tac =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let tac = Value.of_closure ist tac in
   let env = Proofview.Goal.env gl in
   let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in
   let glb_intuition = Tacintern.glob_tactic_env vars env intuition in
@@ -360,8 +359,9 @@ let intuition_gen ist flags tac =
   end }
 
 let tauto_intuitionistic flags =
+  let fail = Value.of_closure (default_ist ()) <:tactic<fail>> in
   Proofview.tclORELSE
-    (intuition_gen (default_ist ()) flags <:tactic<fail>>)
+    (intuition_gen (default_ist ()) flags fail)
     begin function (e, info) -> match e with
       | Refiner.FailError _ | UserError _ ->
           Tacticals.New.tclZEROMSG (str "tauto failed.")
@@ -395,7 +395,8 @@ let tauto_gen flags =
 
 let default_intuition_tac =
   let tac _ _ = Auto.h_auto None [] None in
-  register_tauto_tactic tac "auto_with"
+  let tac = register_tauto_tactic tac "auto_with" in
+  Value.of_closure (default_ist ()) tac
 
 (* This is the uniform mode dealing with ->, not, iff and types isomorphic to
    /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.