From ea85f46dc0cc34db149c24bb2da8f3130e191fc1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 11 Sep 2009 17:53:30 +0000
Subject: Generalized the possibility to refer to a global name by a notation
 string in most commands expecting a global name (e.g. 'Print "+"' for an
 infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly
 surrounded by a scope delimiter). Support for such smart globals in VERNAC
 EXTEND to do.

Added a file smartlocate.ml for high-level globalization functions.

Mini-nettoyage metasyntax.ml.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics/auto.ml')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c62824d4b6..394626f247 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -34,6 +34,7 @@ open Clenv
 open Hiddentac
 open Libnames
 open Nametab
+open Smartlocate
 open Libobject
 open Library
 open Printer
@@ -533,7 +534,7 @@ type hints_entry =
 let interp_hints h =
   let f = Constrintern.interp_constr Evd.empty (Global.env()) in
   let fr r =
-    let gr = Syntax_def.global_with_alias r in
+    let gr = global_with_alias r in
     let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
     r' in
@@ -1118,7 +1119,7 @@ let superauto n to_add argl  =
   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
 
 let interp_to_add gl r =
-  let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
+  let r = locate_global_with_alias (qualid_of_reference r) in
   let id = basename_of_global r in
   (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
 
-- 
cgit v1.2.3