diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 17:53:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-11 17:53:30 +0000 |
| commit | ea85f46dc0cc34db149c24bb2da8f3130e191fc1 (patch) | |
| tree | 3b8fa67f3f1dc5bb2815b38c1040a3ea192c88fe /interp/syntax_def.ml | |
| parent | 7131609a82198080421b15e2c7a0d8f3b6cbd3de (diff) | |
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
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 1619bad27..e58bb000a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -81,29 +81,3 @@ let declare_syntactic_definition local id onlyparse pat = let search_syntactic_definition loc kn = out_pat (KNmap.find kn !syntax_table) - -let global_of_extended_global = function - | TrueGlobal ref -> ref - | SynDef kn -> - match search_syntactic_definition dummy_loc kn with - | [],ARef ref -> ref - | _ -> raise Not_found - -let locate_global_with_alias (loc,qid) = - let ref = Nametab.locate_extended qid in - try global_of_extended_global ref - with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ - str " is bound to a notation that does not denote a reference") - -let global_inductive_with_alias r = - match locate_global_with_alias (qualid_of_reference r) with - | IndRef ind -> ind - | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") - -let global_with_alias r = - let (loc,qid as lqid) = qualid_of_reference r in - try locate_global_with_alias lqid - with Not_found -> Nametab.error_global_not_found_loc loc qid |