Broutilles

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

2 files changed, 16 insertions, 15 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 231aea23a..8435b6d74 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -45,7 +45,7 @@ let rec execute mf env cstr =
 	anomaly "the kernel does not understand existential variables"
 	
     | IsRel n -> 
-	(relative env n, cst0)
+	(relative env Evd.empty n, cst0)
 
     | IsVar id -> 
 	(make_judge cstr (snd (lookup_var id env)), cst0)
@@ -117,8 +117,7 @@ let rec execute mf env cstr =
      | IsProd (name,c1,c2) ->
         let (j,cst1) = execute mf env c1 in
         let varj = type_judgment env Evd.empty j in
-	let var = assumption_of_type_judgment varj in
-	let env1 = push_rel (name,var) env in
+	let env1 = push_rel (name,assumption_of_type_judgment varj) env in
         let (j',cst2) = execute mf env1 c2 in
 	let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -130,7 +129,7 @@ let rec execute mf env cstr =
 	let cst = Constraint.union cst1 cst2 in
         (cast_rel env Evd.empty cj tj, cst)
 	  
-      | _ -> error_cant_execute CCI env cstr
+    | IsXtra _ -> anomaly "Safe_typing: found an Extra"
 	  
 and execute_fix mf env lar lfi vdef =
   let (larj,cst1) = execute_array mf env lar in
@@ -360,7 +359,7 @@ let rec infos_and_sort env t =
 	let logic = not (is_info_type env Evd.empty varj) in
 	let small = is_small s1 in
 	((logic,small) :: infos, smax', cst')
-    | IsCast (c,t) -> infos_and_sort env c
+    | IsCast (c,_) -> infos_and_sort env c
     | _ ->
 	([],prop (* = neutral element of max_universe *),Constraint.empty)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3c5ede554..7edb8680f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -23,28 +23,30 @@ let j_val_only j = j.uj_val
 
 let typed_type_of_judgment env sigma j = j.uj_type
 
+(* This should be a type intended to be assumed *)
 let assumption_of_judgment env sigma j =
   match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
     | DOP0(Sort s) -> make_typed j.uj_val s
     | _ -> error_assumption CCI env j.uj_val
 
-let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
-
+(* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env sigma j =
   match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
     | DOP0(Sort s) -> {utj_val = j.uj_val; utj_type = s }
-    | _ -> error_assumption CCI env j.uj_val
+    | _ -> error_not_type CCI env j
+
+let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
 
 
 (* Type of a de Bruijn index. *)
 	  
-let relative env n = 
+let relative env sigma n = 
   try
     let (_,typ) = lookup_rel n env in
     { uj_val  = Rel n;
       uj_type = typed_app (lift n) typ }
   with Not_found -> 
-    error_unbound_rel CCI env n
+    error_unbound_rel CCI env sigma n
 
 (* Management of context of variables. *)
 
@@ -288,12 +290,11 @@ let abs_rel env sigma name var j =
 let gen_rel env sigma name varj j =
   let var = assumption_of_type_judgment varj in
   match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
-    | DOP0(Sort s) as ts ->
-	let ts = (* mkCast *) j.uj_val (* ts *) in
+    | DOP0(Sort s) ->
 	let (s',g) = sort_of_product varj.utj_type s (universes env) in
 	let res_type = mkSort s' in
 	let (res_kind,g') = type_of_sort res_type in
-        { uj_val = mkProd name (incast_type var) ts;
+        { uj_val = mkProd name (incast_type var) j.uj_val;
           uj_type = make_typed res_type res_kind },
 	g'
     | _ -> 
@@ -301,7 +302,7 @@ let gen_rel env sigma name varj j =
 	  error "Proof objects can only be abstracted" 
 	else
 *)
-	  error_generalization CCI env (name,var) j.uj_val
+	  error_generalization CCI env sigma (name,var) j
 
 (* Type of a cast. *)
 	    
@@ -332,7 +333,8 @@ let apply_rel_list env sigma nocheck argjl funj =
 		   let cst' = Constraint.union cst c in
 		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
 		 with NotConvertible -> 
-		   error_cant_apply_bad_type CCI env (n,body_of_type hj.uj_type,c1)
+		   error_cant_apply_bad_type CCI env sigma
+		     (n,body_of_type hj.uj_type,c1)
 		     funj argjl)
           | _ ->
 	      error_cant_apply_not_functional CCI env funj argjl