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 --- library/nametab.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 5367bfdd8..774b148a5 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] -- cgit v1.2.3