diff options
| -rw-r--r-- | interp/smartlocate.ml | 26 | ||||
| -rw-r--r-- | interp/smartlocate.mli | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 24 insertions, 10 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index c5a28ab2d..7ad5561e3 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -20,6 +20,18 @@ open Misctypes open Syntax_def open Notation_term +let global_of_extended_global_head = function + | TrueGlobal ref -> ref + | SynDef kn -> + let _, syn_def = search_syntactic_definition kn in + let rec head_of = function + | NRef ref -> ref + | NApp (rc, _) -> head_of rc + | NCast (rc, _) -> head_of rc + | NLetIn (_, _, rc) -> head_of rc + | _ -> raise Not_found in + head_of syn_def + let global_of_extended_global = function | TrueGlobal ref -> ref | SynDef kn -> @@ -28,9 +40,11 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias (loc,qid) = +let locate_global_with_alias ?(head=false) (loc,qid) = let ref = Nametab.locate_extended qid in - try global_of_extended_global ref + try + if head then global_of_extended_global_head ref + else 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.") @@ -44,14 +58,14 @@ let global_inductive_with_alias r = pr_reference r ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found_loc loc qid -let global_with_alias r = +let global_with_alias ?head r = let (loc,qid as lqid) = qualid_of_reference r in - try locate_global_with_alias lqid + try locate_global_with_alias ?head lqid with Not_found -> Nametab.error_global_not_found_loc loc qid -let smart_global = function +let smart_global ?head = function | AN r -> - global_with_alias r + global_with_alias ?head r | ByNotation (loc,ntn,sc) -> Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 86aa69681..9006e3687 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -17,7 +17,7 @@ open Misctypes if not bound in the global env; raise a [UserError] if bound to a syntactic def that does not denote a reference *) -val locate_global_with_alias : qualid located -> global_reference +val locate_global_with_alias : ?head:bool -> qualid located -> global_reference (** Extract a global_reference from a reference that can be an "alias" *) val global_of_extended_global : extended_global_reference -> global_reference @@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> global_reference May raise [Nametab.GlobalizationError _] for an unknown reference, or a [UserError] if bound to a syntactic def that does not denote a reference. *) -val global_with_alias : reference -> global_reference +val global_with_alias : ?head:bool -> reference -> global_reference (** The same for inductive types *) val global_inductive_with_alias : reference -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : reference or_by_notation -> global_reference +val smart_global : ?head:bool -> reference or_by_notation -> global_reference (** The same for inductive types *) val smart_global_inductive : reference or_by_notation -> inductive diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b98801ea7..074d260c7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -42,7 +42,7 @@ let prerr_endline = let cl_of_qualid = function | FunClass -> Classops.CL_FUN | SortClass -> Classops.CL_SORT - | RefClass r -> Class.class_of_global (Smartlocate.smart_global r) + | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r) let scope_class_of_qualid qid = Notation.scope_class_of_reference (Smartlocate.smart_global qid) |