Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 10 insertions, 17 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fe7488c21..1ddb7a08b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -114,7 +114,8 @@ let rec execute mf env cstr =
         let varj = type_judgment env Evd.empty j in
 	let env1 = push_rel_assum (name,varj.utj_val) env in
         let (j',cst2) = execute mf env1 c2 in
-	let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
+        let varj' = type_judgment env Evd.empty j' in
+	let (j,cst3) = gen_rel env1 Evd.empty name varj varj' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 860153ef4..dceda45df 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -259,28 +259,20 @@ let abs_rel env sigma name var j =
     uj_type = mkProd (name, var, j.uj_type) },
   Constraint.empty
 
-(* [gen_rel env sigma name (typ1,s1) j] implements the rule
+(* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule
 
-    env |- typ1:s1       env, name:typ |- j.uj_val : j.uj_type
+    env |- typ1:s1       env, name:typ |- typ2 : s2
     -------------------------------------------------------------------------
          s' >= (s1,s2), env |- (name:typ)j.uj_val : s'
 
   where j.uj_type is convertible to a sort s2
 *)
 
-let gen_rel env sigma name {utj_val = t1; utj_type = s1} j =
-  match kind_of_term (whd_betadeltaiota env sigma j.uj_type) with
-    | IsSort s ->
-	let (s',g) = sort_of_product s1 s (universes env) in
-        { uj_val = mkProd (name, t1, j.uj_val);
-          uj_type = mkSort s' },
-	g
-    | _ -> 
-(* 	if is_small (level_of_type j.uj_type) then (* message historique ?? *)
-	  error "Proof objects can only be abstracted" 
-	else
-*)
-	  error_generalization CCI env sigma (name,t1) j
+let gen_rel env sigma name t1 t2 =
+  let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in
+  { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
+    uj_type = mkSort s },
+  g
 
 (* [cast_rel env sigma (typ1,s1) j] implements the rule
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 9f2bde9b8..d51594822 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -55,7 +55,7 @@ val abs_rel :
 
 (*s Type of a product. *)
 val gen_rel :
-  env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment 
+  env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_type_judgment 
     -> unsafe_judgment * constraints
 
 val sort_of_product : sorts -> sorts -> universes -> sorts * constraints