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

5 files changed, 15 insertions, 23 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fe7488c217..1ddb7a08bc 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 860153ef4f..dceda45df4 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 9f2bde9b88..d515948222 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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0ffa66d2e3..b25af668c9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -320,12 +320,10 @@ let rec pretype tycon env isevars lvar lmeta cstr =
 	fst (abs_rel env !isevars name j.utj_val j')
 
     | RBinder(loc,BProd,name,c1,c2)        ->
-	let j = pretype_type empty_tycon env isevars lvar lmeta c1 in
+	let j = pretype_type empty_valcon env isevars lvar lmeta c1 in
 	let var = (name,j.utj_val) in
-	(* Ici, faudrait appeler pretype_type mais gen_rel n'a pas la bonne 
-           interface, tout ca pour preserver le message d'erreur de gen_rel *)
-
-	let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
+	let env' = push_rel_assum var env in
+	let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in
 	let resj =
 	  try fst (gen_rel env !isevars name j j')
 	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 3f0ab9501a..8279fb7e89 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -95,7 +95,8 @@ let rec execute mf env sigma cstr =
         let varj = type_judgment env sigma j in
 	let env1 = push_rel_assum (name,varj.utj_val) env in
         let j' = execute mf env1 sigma c2 in
-	let (j,_) = gen_rel env1 sigma name varj j' in
+        let varj' = type_judgment env sigma j' in
+	let (j,_) = gen_rel env1 sigma name varj varj' in
 	j
 
      | IsLetIn (name,c1,c2,c3) ->