From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 22 Feb 2016 10:32:57 +0100
Subject: 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.
---
 interp/constrarg.ml  | 2 +-
 interp/constrarg.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index b093d92e73..a48d683754 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -25,7 +25,7 @@ let wit_int_or_var =
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
   Genarg.make0 None "intropattern"
 
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   Genarg.make0 None "tactic"
 
 let wit_ident =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index e1a5f4d7c9..5c26af3c2a 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -69,6 +69,6 @@ val wit_red_expr :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-- 
cgit v1.2.3