From 243ffa4b928486122075762da6ce8da707e07daf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 Aug 2014 00:02:45 +0200
Subject: Moving the TacExtend node from atomic to plain tactics.

Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
---
 intf/tacexpr.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 8e5b51b873..b9c41ae03e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -162,9 +162,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
       ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option
   | TacInversion of ('trm,'nam) inversion_strength * quantified_hypothesis
 
-  (* For ML extensions *)
-  | TacExtend of Loc.t * ml_tactic_name * 'lev generic_argument list
-
   (* For syntax extensions *)
   | TacAlias of Loc.t * KerName.t * (Id.t * 'lev generic_argument) list
 
@@ -247,6 +244,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr =
       ('p,('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr) match_rule list
   | TacFun of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast
   | TacArg of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_arg located
+  (* For ML extensions *)
+  | TacML of Loc.t * ml_tactic_name * 'l generic_argument list
 
 and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
     Id.t option list * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr
-- 
cgit v1.2.3