diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/notation.mli | 3 | ||||
| -rw-r--r-- | interp/smartlocate.ml | 8 |
3 files changed, 10 insertions, 9 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 2703930705..fb3cefd624 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1809,10 +1809,10 @@ let browse_notation strict ntn map = map [] in List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l -let global_reference_of_notation test (ntn,(sc,c,_)) = +let global_reference_of_notation ~head test (ntn,(sc,c,_)) = match c with | NRef ref when test ref -> Some (ntn,sc,ref) - | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref -> + | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref -> Some (ntn,sc,ref) | _ -> None @@ -1824,14 +1824,14 @@ let error_notation_not_reference ?loc ntn = (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") -let interp_notation_as_global_reference ?loc test ntn sc = +let interp_notation_as_global_reference ?loc ~head test ntn sc = let scopes = match sc with | Some sc -> let scope = find_scope (find_delimiters_scope sc) in String.Map.add sc scope String.Map.empty | None -> !scope_map in let ntns = browse_notation true ntn scopes in - let refs = List.map (global_reference_of_notation test) ntns in + let refs = List.map (global_reference_of_notation ~head test) ntns in match Option.List.flatten refs with | [_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn diff --git a/interp/notation.mli b/interp/notation.mli index b427aa9bb3..96a76c4de6 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes -> (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> +(** If head is true, also allows applied global references. *) +val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t (** Checks for already existing notations *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 98fa71e15d..03977fcb4e 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -62,15 +62,15 @@ let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function +let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> - global_with_alias ?head r + global_with_alias ~head r | ByNotation (ntn,sc) -> - Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) + Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc) let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_inductive_with_alias r | ByNotation (ntn,sc) -> destIndRef - (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)) + (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc)) |