From ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 17 May 2005 12:43:22 +0000
Subject: Extension de Tactic Notation pour permettre d'tendre et de faire
 rffrence aux niveaux syntaxiques des tacticielles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 7ee45f67de..3eccf3d34f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -187,7 +187,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* For syntax extensions *)
   | TacAlias of loc * string *
       (identifier * ('constr,'tac) generic_argument) list
-      * (dir_path * 'tac)
+      * (dir_path * glob_tactic_expr)
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
@@ -230,6 +230,16 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacFreshId     of string option
   | Tacexp of 'tac
 
+(* Globalized tactics *)
+and glob_tactic_expr =
+    (rawconstr_and_expr,
+     constr_pattern,
+     evaluable_global_reference and_short_name or_var,
+     inductive or_var,
+     ltac_constant located or_var,
+     identifier located,
+     glob_tactic_expr) gen_tactic_expr
+
 type raw_tactic_expr =
     (constr_expr,
      pattern_expr,
@@ -262,16 +272,6 @@ type raw_generic_argument =
 
 type raw_red_expr = (constr_expr, reference) red_expr_gen
 
-(* Globalized tactics *)
-type glob_tactic_expr =
-    (rawconstr_and_expr,
-     constr_pattern,
-     evaluable_global_reference and_short_name or_var,
-     inductive or_var,
-     ltac_constant located or_var,
-     identifier located,
-     glob_tactic_expr) gen_tactic_expr
-
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
      constr_pattern,
-- 
cgit v1.2.3