Merge PR #11918: Fix #11845: anomaly when including partially applied functor

Reviewed-by: ppedrot

1 files changed, 15 insertions, 15 deletions

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