From b847fcc99e35a09b862aa758c5e3f0b08a93202d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 12 Feb 2004 19:35:23 +0000
Subject: Localisation des erreurs d'internalisation des notations de tactiques
 dans le module de leur définition. Error_in_file dans Util et étendu avec
 possibilité de noms de modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 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 cf4741e5e2..c55fc31a85 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -192,7 +192,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
-      * 'tac
+      * (dir_path * 'tac)
 
 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
-- 
cgit v1.2.3