From ab65dd50ee42dd64a8df08ec61fef6da307123ca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Apr 2003 13:22:47 +0000
Subject: Localisation erreurs TacAlias; Globalisation moins tolérante dans les
 définitions de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 0fd4130d24..bdc8f3367c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -165,7 +165,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExtend of loc * string * ('constr,'tac) generic_argument list
 
   (* For syntax extensions *)
-  | TacAlias of string *
+  | TacAlias of loc * string *
       (identifier * ('constr,'tac) generic_argument) list
       * 'tac
 
-- 
cgit v1.2.3