Renoncement à distinguer les types "constr" et "types"; nettoyage

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

2 files changed, 11 insertions, 16 deletions

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e0b802c3e6..321a7b2ec6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -46,14 +46,9 @@ let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
 let pf_hyps gls = (sig_it gls).evar_hyps
 
 let pf_concl gls = (sig_it gls).evar_concl
-(*
-let pf_untyped_hyps gls  =
-  let sign = Environ.named_context (pf_env gls) in
-  map_sign_typ (fun x -> body_of_type x) sign
-*)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
-  List.map (fun (id,_,x) -> (id,body_of_type x)) sign
+  List.map (fun (id,_,x) -> (id, x)) sign
 
 let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
 
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index 55c45dd4d1..584b2c92c2 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -25,14 +25,14 @@ end
 module Make = functor (P : Printer) -> struct
 
   let print_decl k env (s,typ) =
-    let ptyp = P.pr_term k env (body_of_type typ) in 
+    let ptyp = P.pr_term k env typ in 
     (spc () ++ pr_id s ++ str" : " ++ ptyp)
   
   let print_binding k env = function
     | Anonymous,ty -> 
-	(spc () ++ str"_" ++ str" : " ++ P.pr_term k env (body_of_type ty))
+	(spc () ++ str"_" ++ str" : " ++ P.pr_term k env ty)
     | Name id,ty -> 
-	(spc () ++ pr_id id ++ str" : " ++ P.pr_term k env (body_of_type ty))
+	(spc () ++ pr_id id ++ str" : " ++ P.pr_term k env ty)
 
 (****
   let sign_it_with f sign e =
@@ -138,7 +138,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
 
 let explain_generalization k ctx (name,var) c =
   let pe = pr_ne_ctx (str"in environment") k ctx in
-  let pv = P.pr_term k ctx (body_of_type var) in
+  let pv = P.pr_term k ctx var in
   let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
   (str"Illegal generalization: " ++ pe ++ fnl () ++
      str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
@@ -159,13 +159,13 @@ 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_ctx (str"in environment") k ctx in
   let pr = pr_term k ctx rator.uj_val in
-  let prt = pr_term k ctx (body_of_type rator.uj_type) in
+  let prt = pr_term k ctx rator.uj_type 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 = pr_term k ctx c.uj_val in
-		  let pct = pr_term k ctx (body_of_type c.uj_type) in
+		  let pct = pr_term k ctx c.uj_type in
 		  hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
   in
   (str"Illegal application (Type Error): " ++ pe ++ fnl () ++
@@ -181,12 +181,12 @@ let explain_cant_apply_not_functional k ctx rator randl =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_ctx (str"in environment") k ctx in
   let pr = pr_term k ctx rator.uj_val in
-  let prt = pr_term k ctx (body_of_type rator.uj_type) in
+  let prt = pr_term k ctx 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 = pr_term k ctx c.uj_val in
-		  let pct = pr_term k ctx (body_of_type c.uj_type) in
+		  let pct = pr_term k ctx c.uj_type in
 		  hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
   in
   (str"Illegal application (Non-functional construction): " ++ pe ++ fnl () ++
@@ -244,8 +244,8 @@ in
     
 let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
   let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
-  let pvdt = P.pr_term k ctx (body_of_type (vdefj.(i)).uj_type) in
-  let pv = P.pr_term k ctx (body_of_type vargs.(i)) in
+  let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in
+  let pv = P.pr_term k ctx vargs.(i) in
   (str"The " ++
      if Array.length vdefj = 1 then (mt ()) else (int (i+1) ++ str "-th") ++
      str"recursive definition" ++ spc () ++ pvd ++ spc () ++