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

3 files changed, 18 insertions, 2 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index c7d484d1e2..0404d7cd8a 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -23,6 +23,14 @@ type global_reference =
   | ConstructRef of constructor
 
 let isVarRef = function VarRef _ -> true | _ -> false
+let isConstRef = function ConstRef _ -> true | _ -> false
+let isIndRef = function IndRef _ -> true | _ -> false
+let isConstructRef = function ConstructRef _ -> true | _ -> false
+
+let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
+let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
+let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
+let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
 let subst_constructor subst ((kn,i),j as ref) =
   let kn' = subst_kn subst kn in 
diff --git a/library/libnames.mli b/library/libnames.mli
index 92dd9cb280..b93ee87ee1 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -24,6 +24,14 @@ type global_reference =
   | ConstructRef of constructor
 
 val isVarRef : global_reference -> bool
+val isConstRef : global_reference -> bool
+val isIndRef : global_reference -> bool
+val isConstructRef : global_reference -> bool
+
+val destVarRef : global_reference -> variable
+val destConstRef : global_reference -> constant
+val destIndRef : global_reference -> inductive
+val destConstructRef : global_reference -> constructor
 
 val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
diff --git a/library/nametab.mli b/library/nametab.mli
index 5367bfdd86..774b148a56 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -21,12 +21,12 @@ open Libnames
     There are three classes of names:
 
     1a- internal kernel names: [kernel_name], [constant], [inductive],
-        [module_path]
+        [module_path], [dir_path]
 
     1b- other internal names: [global_reference], [syndef_name],
         [extended_global_reference], [global_dir_reference], ...
 
-    2- full, non ambiguous user names: [full_path] and [dir_path]
+    2- full, non ambiguous user names: [full_path]
 
     3- non necessarily full, possibly ambiguous user names: [reference]
        and [qualid]