cleanup: less exceptions, removal of try_interp_name_alias

9 files changed, 86 insertions, 77 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f02874253e..e72b73c36e 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -283,10 +283,13 @@ let local_binders_loc bll = match bll with
 
 (** Folds and maps *)
 let is_constructor id =
-  try Globnames.isConstructRef
-        (Smartlocate.global_of_extended_global
-           (Nametab.locate_extended (qualid_of_ident id)))
-  with Not_found -> false
+  match
+    Smartlocate.global_of_extended_global
+      (Nametab.locate_extended (qualid_of_ident id))
+  with
+  | exception Not_found -> false
+  | None -> false
+  | Some gref -> Globnames.isConstructRef gref
 
 let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
   | CPatRecord l ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 958e1408f8..3d4b6c40cb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1121,23 +1121,54 @@ let dump_extended_global loc = function
 let intern_extended_global_of_qualid qid =
   let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
 
-let intern_reference qid =
-  let r =
-    try intern_extended_global_of_qualid qid
-    with Not_found as exn ->
-      let _, info = Exninfo.capture exn in
-      Nametab.error_global_not_found ~info qid
-  in
-  Smartlocate.global_of_extended_global r
+let intern_sort_name ~local_univs = function
+  | CSProp -> GSProp
+  | CProp -> GProp
+  | CSet -> GSet
+  | CRawType u -> GRawUniv u
+  | CType qid ->
+    let is_id = qualid_is_ident qid in
+    let local = if not is_id then None
+      else Id.Map.find_opt (qualid_basename qid) local_univs.bound
+    in
+    match local with
+    | Some u -> GUniv u
+    | None ->
+      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
+      with Not_found ->
+        if is_id && local_univs.unb_univs
+        then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
+        else
+          CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
+
+let intern_sort ~local_univs s =
+  map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
+
+let intern_instance ~local_univs us =
+  Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
+
+let intern_name_alias = function
+  | { CAst.v = CRef(qid,u) } ->
+      let r =
+        try Some (intern_extended_global_of_qualid qid)
+        with Not_found -> None
+      in
+      Option.bind r Smartlocate.global_of_extended_global |>
+      Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u)
+  | _ -> None
 
 let intern_projection qid =
-  try
-    match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with
-    | GlobRef.ConstRef c as gr ->
-        (gr, Structure.find_from_projection c)
-    | _ -> raise Not_found
-  with Not_found ->
-    Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  match
+    Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |>
+    Option.map (function
+     | GlobRef.ConstRef c as x -> x, Structure.find_from_projection c
+     | _ -> raise Not_found)
+  with
+  | exception Not_found ->
+     Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  | None ->
+     Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+  | Some x -> x
 
 (**********************************************************************)
 (* Interpreting references                                            *)
@@ -1182,37 +1213,6 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
   | UAnonymous {rigid} -> UAnonymous {rigid}
   | UNamed id -> UNamed [id,0]
 
-let intern_sort_name ~local_univs = function
-  | CSProp -> GSProp
-  | CProp -> GProp
-  | CSet -> GSet
-  | CRawType u -> GRawUniv u
-  | CType qid ->
-    let is_id = qualid_is_ident qid in
-    let local = if not is_id then None
-      else Id.Map.find_opt (qualid_basename qid) local_univs.bound
-    in
-    match local with
-    | Some u -> GUniv u
-    | None ->
-      try GUniv (Univ.Level.make (Nametab.locate_universe qid))
-      with Not_found ->
-        if is_id && local_univs.unb_univs
-        then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
-        else
-          CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
-
-let intern_sort ~local_univs s =
-  map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
-
-let intern_instance ~local_univs us =
-  Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
-
-let try_interp_name_alias = function
-  | [], { CAst.v = CRef (ref,u) } ->
-     NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u)
-  | _ -> raise Not_found
-
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   let loc = qid.loc in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 65b63962d0..7c1e658ff1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -147,12 +147,9 @@ val interp_constr_pattern :
   env -> evar_map -> ?expected_type:typing_constraint ->
     constr_pattern_expr -> constr_pattern
 
-(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : qualid -> GlobRef.t
-
-(** For syntactic definitions: check if abbreviation to a name
-    and avoid early insertion of maximal implicit arguments *)
-val try_interp_name_alias : 'a list * constr_expr -> notation_constr
+(** Returns None if not a reference or a syndef not bound to a name *)
+val intern_name_alias :
+  constr_expr -> (GlobRef.t * Glob_term.glob_level list option) option
 
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> qualid -> glob_constr
@@ -174,7 +171,7 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition
    (these functions do not modify the glob file) *)
 
-val locate_reference :  Libnames.qualid -> GlobRef.t
+val locate_reference :  Libnames.qualid -> GlobRef.t option
 val is_global : Id.t -> bool
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
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
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 26f2a4f36d..abf9839c9e 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -19,8 +19,9 @@ open Globnames
 
 val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
-(** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> GlobRef.t
+(** Extract a global_reference from a reference that can be an "alias".
+    If the reference points to a more complex term, we return None *)
+val global_of_extended_global : extended_global_reference -> GlobRef.t option
 
 (** Locate a reference taking into account possible "alias" notations.
     May raise [Nametab.GlobalizationError _] for an unknown reference,
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3234d40f73..7d19c443e9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
           (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
           let evd', res =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference
-                 (qualid_of_ident equation_lemma_id))
+              (Option.get (Constrintern.locate_reference
+                 (qualid_of_ident equation_lemma_id)))
           in
           evd := evd';
           let sigma, _ =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc..5980446508 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -241,7 +241,7 @@ let change_property_sort evd toSort princ princName =
   in
   let evd, princName_as_constr =
     Evd.fresh_global (Global.env ()) evd
-      (Constrintern.locate_reference (Libnames.qualid_of_ident princName))
+      (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident princName)))
   in
   let init =
     let nargs =
@@ -408,8 +408,8 @@ let register_struct is_rec fixpoint_exprl =
         (fun (evd, l) {Vernacexpr.fname} ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference
-                 (Libnames.qualid_of_ident fname.CAst.v))
+              (Option.get (Constrintern.locate_reference
+                 (Libnames.qualid_of_ident fname.CAst.v)))
           in
           let cst, u = destConst evd c in
           let u = EInstance.kind evd u in
@@ -427,8 +427,8 @@ let register_struct is_rec fixpoint_exprl =
         (fun (evd, l) {Vernacexpr.fname} ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference
-                 (Libnames.qualid_of_ident fname.CAst.v))
+              (Option.get (Constrintern.locate_reference
+                 (Libnames.qualid_of_ident fname.CAst.v)))
           in
           let cst, u = destConst evd c in
           let u = EInstance.kind evd u in
@@ -1522,7 +1522,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
           let _, lem_cst_constr =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
           in
           let lem_cst, _ = EConstr.destConst !evd lem_cst_constr in
           update_Function {finfo with correctness_lemma = Some lem_cst})
@@ -1592,7 +1592,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           in
           let _, lem_cst_constr =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)))
           in
           let lem_cst, _ = destConst !evd lem_cst_constr in
           update_Function {finfo with completeness_lemma = Some lem_cst})
@@ -1615,7 +1615,7 @@ let derive_inversion fix_names =
         (fun id (evd, l) ->
           let evd, c =
             Evd.fresh_global (Global.env ()) evd
-              (Constrintern.locate_reference (Libnames.qualid_of_ident id))
+              (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id)))
           in
           let cst, u = EConstr.destConst evd c in
           (evd, (cst, EConstr.EInstance.kind evd u) :: l))
@@ -1635,8 +1635,8 @@ let derive_inversion fix_names =
           (fun id (evd, l) ->
             let evd, id =
               Evd.fresh_global (Global.env ()) evd
-                (Constrintern.locate_reference
-                   (Libnames.qualid_of_ident (mk_rel_id id)))
+                (Option.get (Constrintern.locate_reference
+                   (Libnames.qualid_of_ident (mk_rel_id id))))
             in
             (evd, fst (EConstr.destInd evd id) :: l))
           fix_names (evd', [])
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4e0e2dc501..1221ad0bda 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat =
                   (elimination_sort_of_goal gl)
               in
               let princ_ref =
-                try
+                match
                   Constrintern.locate_reference
                     (Libnames.qualid_of_ident princ_name)
-                with Not_found ->
+                with
+                | Some r -> r
+                | None ->
                   user_err
                     ( str "Cannot find induction principle for "
                     ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f9f65a8c30..692f1d7388 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1795,8 +1795,10 @@ let add_class_scope local scope cl =
 
 let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
   let acvars,pat,reversibility =
-    try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
-    with Not_found ->
+    match vars, intern_name_alias c with
+    | [], Some(r,u) ->
+      Id.Map.empty, NRef(r, u), APrioriReversible
+    | _ ->
       let fold accu id = Id.Map.add id NtnInternTypeAny accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
       let nenv = {