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
---
 translate/pptacticnew.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'translate')

diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 44224227d1..acff5e1648 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -202,7 +202,7 @@ let rec pr_atom0 env = function
 and pr_atom1 env = function
   | TacExtend (_,s,l) ->
       pr_extend (pr_constr env) (pr_tac env) s l
-  | TacAlias (s,l,_) ->
+  | TacAlias (_,s,l,_) ->
       pr_extend (pr_constr env) (pr_tac env) s (List.map snd l)
 
   (* Basic tactics *)
-- 
cgit v1.2.3