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

2 files changed, 5 insertions, 13 deletions

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)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5df025c1a2..28173b7a34 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -26,6 +26,7 @@ open Names
 open Nameops
 open Libnames
 open Nametab
+open Smartlocate
 open Pfedit
 open Proof_type
 open Refiner
@@ -365,17 +366,7 @@ let intern_or_var ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
   | ArgArg _ as x -> x
 
-let loc_of_by_notation f = function
-  | AN c -> f c
-  | ByNotation (loc,s,_) -> loc
-
-let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
-
-let intern_inductive_or_by_notation = function
-  | AN r -> Nametab.global_inductive r
-  | ByNotation (loc,ntn,sc) ->
-      destIndRef (Notation.interp_notation_as_global_reference loc
-        (function IndRef ind -> true | _ -> false) ntn sc)
+let intern_inductive_or_by_notation = smart_global_inductive
 
 let intern_inductive ist = function
   | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)