Merge PR #13965: [abbreviation] user syntax to set interp scope of argument

Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot

1 files changed, 6 insertions, 2 deletions

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 91d05f7317..56b3cd9815 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -33,7 +33,7 @@ let global_of_extended_global_head = function
         | _ -> raise Not_found in
       head_of syn_def
 
-let global_of_extended_global = function
+let global_of_extended_global_exn = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
   match search_syntactic_definition kn with
@@ -45,11 +45,15 @@ let locate_global_with_alias ?(head=false) qid =
   let ref = Nametab.locate_extended qid in
   try
     if head then global_of_extended_global_head ref
-    else global_of_extended_global ref
+    else global_of_extended_global_exn ref
   with Not_found ->
     user_err ?loc:qid.CAst.loc (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
+let global_of_extended_global x =
+  try Some (global_of_extended_global_exn x)
+  with Not_found -> None
+
 let global_constant_with_alias qid  =
   try match locate_global_with_alias qid with
   | Names.GlobRef.ConstRef c -> c