Nettoyage Coercion

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

4 files changed, 26 insertions, 35 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a4dfa3683..08f46aef5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -54,7 +54,7 @@ let apply_coercion env p hj typ_cl =
               let argl = (class_args_of typ_cl)@[ja.uj_val] in
               let jres = apply_coercion_args env argl fv in
               (if b then 
-		 { uj_val=ja.uj_val; uj_type=jres.uj_type }
+		 { uj_val = ja.uj_val; uj_type = jres.uj_type }
                else 
 		 jres),
 	      jres.uj_type)
@@ -80,13 +80,7 @@ let inh_tosort_force env isevars j =
   with Not_found -> 
     j
 
-let inh_tosort env isevars j = 
-  let typ = whd_betadeltaiota env !isevars j.uj_type in
-  match kind_of_term typ with
-    | IsSort _ -> j  (* idem inh_app_fun *)
-    | _ -> inh_tosort_force env isevars j
-
-let inh_ass_of_j env isevars j =
+let inh_coerce_to_sort env isevars j =
   let typ = whd_betadeltaiota env !isevars j.uj_type in
   match kind_of_term typ with
     | IsSort s -> { utj_val = j.uj_val; utj_type = s }
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 0969387fb..6c257ab69 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -13,15 +13,10 @@ open Evarutil
 
 val inh_app_fun :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_tosort_force :
-  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-
-(* [inh_tosort env sigma j] insert a coercion into [j], if needed, in
-   such a way [t] reduces to a sort; it fails if no coercion is applicable *)
-val inh_tosort :
-  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 
-val inh_ass_of_j :
+(* [inh_coerce_to_sort env sigma j] insert a coercion into [j], if needed, in
+   such a way it gets as type a sort; it fails if no coercion is applicable *)
+val inh_coerce_to_sort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
 
 (* [inh_conv_coerce_to loc env sigma j t] insert a coercion into [j],
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ff10083ff..2ae6d435a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -224,7 +224,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | RRec (loc,fixkind,lfi,lar,vdef) ->
   let larj = Array.map (pretype_type empty_valcon env isevars lvar lmeta) lar in
-  let lara = Array.map (assumption_of_judgment env !isevars) larj in
+  let lara = Array.map (fun a -> a.utj_val) larj in
   let nbfix = Array.length lfi in
   let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in
   let newenv =
@@ -234,7 +234,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     Array.mapi 
       (fun i def -> (* we lift nbfix times the type in tycon, because of
                      * the nbfix variables pushed to newenv *)
-        pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
+        pretype (mk_tycon (lift nbfix (larj.(i).utj_val))) newenv isevars lvar
           lmeta def) vdef in
   (evar_type_fixpoint env isevars lfi lara vdefj;
    match fixkind with
@@ -265,15 +265,14 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let (dom,rng) = split_tycon loc env isevars tycon in
     let dom_valcon = valcon_of_tycon dom in
     let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
-    let assum = (inh_ass_of_j env isevars j).utj_val in
-    let var = (name,assum) in
+    let var = (name,j.utj_val) in
     let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
     in 
-    fst (abs_rel env !isevars name assum j')
+    fst (abs_rel env !isevars name j.utj_val j')
 
 | RBinder(loc,BProd,name,c1,c2)        ->
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
-    let assum = inh_ass_of_j env isevars j in
+    let assum = inh_coerce_to_sort env isevars j in
     let var = (name,assum.utj_val) in
     let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
     (try fst (gen_rel env !isevars name assum j')
@@ -298,7 +297,9 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	try match tycon with
 	    Some pred -> 
 	      let predj = Retyping.get_judgment_of env !isevars pred in
-	      inh_tosort env isevars predj
+	      let tj = inh_coerce_to_sort env isevars predj in (* Utile ?? *)
+	      let { utj_val = v; utj_type = s } = tj in
+	      { uj_val = v; uj_type = mkSort s }
 	  | None -> error "notype"
 	with UserError _ -> (* get type information from type of branches *)
 	  let expbr = Cases.branch_scheme env isevars isrec indf in
@@ -358,32 +359,34 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 
 | RCast(loc,c,t) ->
   let tj = pretype_type (valcon_of_tycon tycon) env isevars lvar lmeta t in
-  let tj = type_judgment env !isevars tj in
   let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
   match tycon with
     | None  -> cj
     | Some t' -> inh_conv_coerce_to loc env isevars cj t'
 
+(* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar lmeta = function
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
     (match valcon with
-       | Some v -> Retyping.get_judgment_of env !isevars v
+       | Some v ->
+	   { utj_val = v;
+	     utj_type = Retyping.get_sort_of env !isevars v }
        | None ->
-	   { uj_val = new_isevar isevars env dummy_sort CCI;
-	     uj_type = dummy_sort })
+	   { utj_val = new_isevar isevars env dummy_sort CCI;
+	     utj_type = Type Univ.dummy_univ })
 | c ->
   let j = pretype empty_tycon env isevars lvar lmeta c in
-  let tj = inh_tosort env isevars j in
+  let tj = inh_coerce_to_sort env isevars j in
   match valcon with
     | None -> tj
     | Some v ->
-	if the_conv_x_leq env isevars v tj.uj_val
+	if the_conv_x_leq env isevars v tj.utj_val
 	then
-	  { uj_val = nf_ise1 !isevars tj.uj_val;
-	    uj_type = tj.uj_type }
+	  { utj_val = nf_ise1 !isevars tj.utj_val;
+	    utj_type = tj.utj_type }
 	else
-	  error_unexpected_type_loc (loc_of_rawconstr c) env tj.uj_val v
+	  error_unexpected_type_loc (loc_of_rawconstr c) env tj.utj_val v
 
 
 let unsafe_infer tycon isevars env lvar lmeta constr =
@@ -456,8 +459,7 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
   let isevars = ref sigma in
-  let j = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
-  let tj = inh_ass_of_j env isevars j in
+  let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
   let metamap = ref [] in
   let v = process_evars fail_evar sigma !isevars metamap tj.utj_val in
   !metamap, {utj_val = v; utj_type = tj.utj_type }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 04995dcb5..c7d1665c7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -61,5 +61,5 @@ val pretype :
 val pretype_type : 
   val_constraint -> env -> 'a evar_defs ->
     (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list ->
-    rawconstr -> unsafe_judgment
+    rawconstr -> unsafe_type_judgment
 (*i*)