diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/syntax_def.ml | 18 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 17 |
2 files changed, 26 insertions, 9 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 3769362b17..b81e7e6c8c 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -79,14 +79,24 @@ let rec set_loc loc _ a = let search_syntactic_definition loc kn = set_loc loc () (KNmap.find kn !syntax_table) -exception BoundToASyntacticDefThatIsNotARef - -let locate_global qid = +let locate_global_with_alias (loc,qid) = match Nametab.extended_locate qid with | TrueGlobal ref -> ref | SyntacticDef kn -> match search_syntactic_definition dummy_loc kn with | Rawterm.RRef (_,ref) -> ref | _ -> - errorlabstrm "" (pr_qualid qid ++ + user_err_loc (loc,"",pr_qualid qid ++ str " is bound to a notation that does not denote a reference") + +let inductive_of_reference_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 diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 50f2f3e7d7..e83cb8885f 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,6 +13,7 @@ open Util open Names open Topconstr open Rawterm +open Libnames (*i*) (* Syntactic definitions. *) @@ -23,10 +24,16 @@ val declare_syntactic_definition : bool -> identifier -> bool -> aconstr val search_syntactic_definition : loc -> kernel_name -> rawconstr -(* [locate_global] locates global reference possibly following a chain of - syntactic aliases; raise Not_found if not bound in the global env; - raise an error if bound to a syntactic def that does not denote a - reference *) +(* [locate_global_with_alias] locates global reference possibly following + a notation if this notation has a role of aliasing; raise Not_found + if not bound in the global env; raise an error if bound to a + syntactic def that does not denote a reference *) -val locate_global : Libnames.qualid -> Libnames.global_reference +val locate_global_with_alias : qualid located -> global_reference + +(* Locate a reference taking into account possible "alias" notations *) +val global_with_alias : reference -> global_reference + +(* The same for inductive types *) +val inductive_of_reference_with_alias : reference -> inductive |