From a4d6176698f761cfd90ee63f051477c5386d657d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 26 Mar 2020 13:01:12 +0100
Subject: Fix #11845: anomaly when including partially applied functor

---
 kernel/modops.ml | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5dd5499a26..301af328e4 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -382,21 +382,21 @@ let inline_delta_resolver env inl mp mbid mtb delta =
   let rec make_inline delta = function
     | [] -> delta
     | (lev,kn)::r ->
-        let kn = replace_mp_in_kn (MPbound mbid) mp kn in
-        let con = constant_of_delta_kn delta kn in
-        try
-          let constant = lookup_constant con env in
-          let l = make_inline delta r in
-          match constant.const_body with
-            | Undef _ | OpaqueDef _ | Primitive _ -> l
-            | Def body ->
-              let constr = Mod_subst.force_constr body in
-              let ctx = Declareops.constant_polymorphic_context constant in
-              let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
-              add_inline_delta_resolver kn (lev, Some constr) l
-        with Not_found ->
-          error_no_such_label_sub (Constant.label con)
-            (ModPath.to_string (Constant.modpath con))
+      let kn = replace_mp_in_kn (MPbound mbid) mp kn in
+      let con = constant_of_delta_kn delta kn in
+      if not (Environ.mem_constant con env) then
+        error_no_such_label_sub (Constant.label con)
+          (ModPath.to_string (Constant.modpath con))
+      else
+        let constant = lookup_constant con env in
+        let l = make_inline delta r in
+        match constant.const_body with
+        | Undef _ | OpaqueDef _ | Primitive _ -> l
+        | Def body ->
+          let constr = Mod_subst.force_constr body in
+          let ctx = Declareops.constant_polymorphic_context constant in
+          let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
+          add_inline_delta_resolver kn (lev, Some constr) l
   in
   make_inline delta constants
 
-- 
cgit v1.2.3