From 4f4c8cdf837763ab8ebc5988f37b8b63f8a284e3 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 13 Nov 2009 10:39:10 +0000
Subject: the inlining computation at functor application was raising not_found
 when the applied module did not fulfill the signature of the functor
 argument. Now Coq gives an understandable error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12515 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 7ee48c352b..2cc0f17ea9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -363,17 +363,21 @@ let complete_inline_delta_resolver env mp mbid mtb delta =
 	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
 	let con = constant_of_kn kn in
 	let con' = constant_of_delta delta con in
-	let constant = lookup_constant con' env in
-	  if (not constant.Declarations.const_opaque) then
-	    let constr = Option.map Declarations.force 
-	      constant.Declarations.const_body in
-	      if constr = None then 
-		(make_inline delta r)
+	  try
+	    let constant = lookup_constant con' env in
+	      if (not constant.Declarations.const_opaque) then
+		let constr = Option.map Declarations.force 
+		  constant.Declarations.const_body in
+		  if constr = None then 
+		    (make_inline delta r)
+		  else
+		    add_inline_constr_delta_resolver con (Option.get constr)
+		      (make_inline delta r)
 	      else
-		add_inline_constr_delta_resolver con (Option.get constr)
-		  (make_inline delta r)
-	  else
-	    (make_inline delta r)
+		(make_inline delta r)
+	  with 
+	      Not_found -> error_no_such_label_sub (con_label con) 
+		(string_of_mp (con_modpath con))
   in
     make_inline delta constants
 
-- 
cgit v1.2.3