From e50a6195097c0d15c839c5403c1d02511afd54e4 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Mon, 19 Apr 2021 11:08:03 +0200
Subject: Check for existence before using `Global.lookup_constant` instead of
 catching `Not_found`

`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
---
 kernel/inductive.ml  | 2 +-
 kernel/inductive.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

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 } *)
-- 
cgit v1.2.3