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.

7 files changed, 21 insertions, 25 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 79ef3d186..9d78a51ef 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -99,4 +99,4 @@ type proof_instr =
     (Term.constr statement,
      Term.constr,
      proof_pattern,
-     Tacexpr.glob_tactic_expr) gen_proof_instr
+     Genarg.Val.t) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 7cfca53c5..4874552d6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 
 let interp_cut interp_it env sigma cut=
   let nenv,nstat = interp_it env sigma cut.cut_stat in
-    {cut with
+    { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using;
        cut_stat=nstat;
        cut_by=interp_justification_items nenv sigma cut.cut_by}
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index adfcb3e60..090b293f5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -496,7 +496,7 @@ let just_tac _then cut info gls0 =
         None ->
 	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
     justification (tclTHEN items_tac method_tac) gls0
 
 let instr_cut mkstat _thus _then cut gls0 =
@@ -546,7 +546,7 @@ let instr_rew _thus rew_side cut gls0 =
         None ->
 	  Proofview.V82.of_tactic automation_tac gls
       | Some tac ->
-	  Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+	  Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
   let just_tac gls =
     justification (tclTHEN items_tac method_tac) gls in
   let (c_id,_) = match cut.cut_stat.st_label with
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 25509b4b5..3e8be3699 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -135,17 +135,17 @@ END
 
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ]
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
-      [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ]
+      [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ]
+     [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ]
 END
 
 open Proofview.Notations
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index fdc5c2bbd..7a3d7936a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -17,15 +17,14 @@ open Quote
 DECLARE PLUGIN "quote_plugin"
 
 let loc = Loc.ghost
-let cont = (loc, Id.of_string "cont")
-let x = (loc, Id.of_string "x")
+let cont = Id.of_string "cont"
+let x = Id.of_string "x"
 
-let make_cont (k : glob_tactic_expr) (c : Constr.t) =
+let make_cont (k : Genarg.Val.t) (c : Constr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (loc, ArgVar cont, [Reference (ArgVar x)]) in
-  let tac = TacLetIn (false, [(cont, Tacexp k)], TacArg (loc, tac)) in
-  let ist = { lfun = Id.Map.singleton (snd x) c; extra = TacStore.empty; } in
-  Tacinterp.eval_tactic_ist ist tac
+  let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
+  let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
+  Tacinterp.eval_tactic_ist ist (TacArg (loc, tac))
 
 TACTIC EXTEND quote
   [ "quote" ident(f) ] -> [ quote f [] ]
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a67cc7cb8..37a895976 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -176,19 +176,16 @@ let ltac_call tac (args:glob_tactic_arg list) =
 let ltac_lcall tac args =
   TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
 
-let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2)
-
-let ltac_apply (f:glob_tactic_expr) (args: Tacinterp.Value.t list) =
+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 (Loc.ghost, 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_letin ("F", Tacexp f) (ltac_lcall "F" args))
+  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
 
 let ltac_record flds =
   TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
@@ -774,7 +771,7 @@ let ltac_ring_structure e =
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
-let ring_lookup (f:glob_tactic_expr) lH rl t =
+let ring_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
@@ -1046,7 +1043,7 @@ let ltac_field_structure e =
   [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
-let field_lookup (f:glob_tactic_expr) lH rl t =
+let field_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 4bd3383d6..07a1ae833 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr
 val from_name : ring_info Spmap.t ref
 
 val ring_lookup :
-  glob_tactic_expr ->
+  Genarg.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic
 
@@ -73,6 +73,6 @@ val add_field_theory :
 val field_from_name : field_info Spmap.t ref
 
 val field_lookup :
-  glob_tactic_expr ->
+  Genarg.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic