Merge PR #14131: Check for existence before using `Global.lookup_constant` instead of catching `Not_found`

Reviewed-by: ppedrot

6 files changed, 28 insertions, 12 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ddbd5fa0a7..13044958dc 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -23,7 +23,7 @@ open Context.Rel.Declaration
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
-(* raise Not_found if not an inductive type *)
+(* raises an anomaly if not an inductive type *)
 let lookup_mind_specif env (kn,tyi) =
   let mib = Environ.lookup_mind kn env in
   if tyi >= Array.length mib.mind_packets then
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 5808a3fa65..4afc7c439a 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -30,7 +30,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 
 (** {6 ... } *)
 (** Fetching information in the environment about an inductive type.
-    Raises [Not_found] if the inductive type is not found. *)
+    Raises an anomaly if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
 
 (** {6 Functions to build standard types related to inductive } *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index cfdaac710b..268d4bf9e9 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1525,8 +1525,7 @@ let inline_test r t =
   else
     let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
     let has_body =
-      try constant_has_body (Global.lookup_constant c)
-      with Not_found -> false
+      Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c)
     in
     has_body &&
       (let t1 = eta_red t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc..6236a5147d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) =
   let sigma = Evd.from_env env in
   let c, c_body =
     match f_ref with
-    | GlobRef.ConstRef c -> (
-      try (c, Global.lookup_constant c)
-      with Not_found ->
+    | GlobRef.ConstRef c ->
+      if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else
         CErrors.user_err
           Pp.(
             str "Cannot find "
-            ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) )
+            ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
     | _ -> CErrors.user_err Pp.(str "Not a function reference")
   in
   match Global.body_of_constant_body Library.indirect_accessor c_body with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 633b9da053..497ce4ae1a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -379,11 +379,10 @@ let find_elim hdcncl lft2rgt dep cls ot =
             let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
             let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
             let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
-            try
-              let _ = Global.lookup_constant c1' in c1'
-            with Not_found ->
+            if not (Environ.mem_constant c1' (Global.env ())) then
               user_err ~hdr:"Equality.find_elim"
-                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
+                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".");
+            c1'
           end
         | _ ->
           begin match if is_eq then eq_elimination_ref false sort else None with
diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v
new file mode 100644
index 0000000000..611464458e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14131.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Unset Elimination Schemes.
+
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
+    JMeq_refl : JMeq x x.
+
+Set Elimination Schemes.
+
+Register JMeq as core.JMeq.type.
+
+Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+  P x -> forall y, JMeq x y -> P y.
+
+Register JMeq_ind as core.JMeq.ind.
+
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+   P x -> forall y, JMeq y x -> P y.
+Proof. intros. try rewrite H0.
+Abort.