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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.mli')

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