From 1de052a2415a70bf4e06be02bff60bee19c013cb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2003 12:23:39 +0000
Subject: Localisation des appels de tactiques définies sans arguments

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 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 157999b108..0cc3234c27 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -519,7 +519,7 @@ let rec glob_printers =
      Printer.pr_pattern,
      pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)),
      (fun vars -> pr_or_var (pr_inductive vars)),
-     pr_or_var pr_ltac_constant,
+     pr_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
      Pptactic.pr_glob_extend)
 
-- 
cgit v1.2.3