Mise en place d'un choix constr/typed_type en remplacement de certains Cast

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

2 files changed, 16 insertions, 25 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 67ecd9139b..820100f6fc 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -27,15 +27,7 @@ let recalc_sp sp =
 let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
 
 let generalize_type id var c =
-  let c' = mkProd (Name id) (body_of_type var) (subst_var id (body_of_type c)) in
-  let c'ty = sort_of_product_without_univ (level_of_type var) (level_of_type c) in 
-  make_typed c' c'ty
-
-let casted_generalize id var c =
-  let c' = mkProd (Name id) (body_of_type var) (subst_var id (cast_term c)) in
-  let s = destSort (whd_all (cast_type c)) in
-  let c'ty = sort_of_product_without_univ (level_of_type var) s in 
-  mkCast c' (DOP0 (Sort c'ty))
+  typed_product_without_universes (Name id) var (typed_app (subst_var id) c)
 
 type modification_action = ABSTRACT | ERASE
 
@@ -116,7 +108,9 @@ let abstract_inductive ids_to_abs hyps inds =
       	(function (tname,arity,cnames,lc) -> 
 	   let arity' = generalize_type id ty arity in
 	   let lc' =
-	     List.map (fun b-> casted_generalize id ty (substl new_refs b)) lc
+	     List.map
+	       (fun b -> generalize_type id ty (typed_app (substl new_refs) b))
+	       lc
 	   in
            (tname,arity',cnames,lc'))
       	inds
@@ -132,7 +126,10 @@ let abstract_inductive ids_to_abs hyps inds =
   in
   let (_,inds',revmodl) =
     List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
-  let inds'' = List.map (fun (a,b,c,d) -> (a,body_of_type b,c,d)) inds' in
+  let inds'' =
+    List.map 
+      (fun (a,b,c,d) -> (a,body_of_type b,c,List.map body_of_type d))
+      inds' in
   (inds'', List.rev revmodl)
 
 let abstract_constant ids_to_abs hyps (body,typ) =
@@ -151,10 +148,7 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 	    Some (ref (Recipe 
 			 (fun () -> mkLambda name cvar (subst_var id (f())))))
       in
-      let typ' = make_typed
-    	(mkProd name cvar (subst_var id (body_of_type typ)))
-	(sort_of_product_without_univ (level_of_type var) (level_of_type typ))
-      in
+      let typ' = generalize_type id var typ in
       (tl_sign hyps,body',typ',ABSTRACT::modl)
   in
   let (_,body',typ',revmodl) =
@@ -213,7 +207,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
 	 (mip.mind_typename,
 	  expmod_type oldenv modlist mip.mind_arity,
 	  Array.to_list mip.mind_consnames,
-	  array_map_to_list (expmod_constr oldenv modlist) mip.mind_lc))
+	  array_map_to_list (expmod_type oldenv modlist) mip.mind_lc))
       mib.mind_packets
   in
   let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b824c20abf..28df858fdf 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -97,7 +97,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
 let explain_generalization k ctx (name,var) c =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
-  let pv = prterm_env ctx (body_of_type var) in
+  let pv = prtype_env ctx var in
   let pc = prterm_env (add_rel (name,var) ctx) c in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
@@ -118,14 +118,12 @@ let explain_actual_type k ctx c ct pt =
 let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
-  let pr = prterm_env ctx rator.uj_val in
-  let prt = prterm_env ctx rator.uj_type in
+  let pr,prt = prjudge_env ctx rator in
   let term_string = if List.length randl > 1 then "terms" else "term" in
   let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
-		  let pc = prterm_env ctx c.uj_val in
-		  let pct = prterm_env ctx c.uj_type in
+		  let pc,pct = prjudge_env ctx c in
 		  hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
   in
   [< 'sTR"Illegal application (Type Error): "; pe; 'fNL;
@@ -141,12 +139,12 @@ let explain_cant_apply_not_functional k ctx rator randl =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
   let pr = prterm_env ctx rator.uj_val in
-  let prt = prterm_env ctx rator.uj_type in
+  let prt = prterm_env ctx (body_of_type rator.uj_type) in
   let term_string = if List.length randl > 1 then "terms" else "term" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
 		  let pc = prterm_env ctx c.uj_val in
-		  let pct = prterm_env ctx c.uj_type in
+		  let pct = prterm_env ctx (body_of_type c.uj_type) in
 		  hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl
   in
   [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL;
@@ -167,8 +165,7 @@ let explain_ill_formed_rec_body k ctx str lna i vdefs =
      'sTR "is not well-formed" >]
     
 let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
-  let pvd = prterm_env ctx (vdefj.(i)).uj_val in
-  let pvdt = prterm_env ctx (vdefj.(i)).uj_type in
+  let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
   let pv = prterm_env ctx (body_of_type vargs.(i)) in
   [< 'sTR"The " ;
      if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];