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

Reviewed-by: ppedrot

1 files changed, 19 insertions, 0 deletions

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.