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

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

4 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 849ee225b..f7c739fe6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -84,10 +84,10 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 		    (crec (push_rel (Anonymous,None,t) env)
 		       (List.rev (lift_rel_context 1 (List.rev rea)),reca))
               | _ -> crec (push_rel d env) (rea,reca) in
-          mkProd (name, body_of_type c, d)
+          mkProd (name,  c, d)
 
       | (name,Some b,c as d)::rea, reca -> 
-	  mkLetIn (name,b,body_of_type c,crec (push_rel d env) (rea,reca))
+	  mkLetIn (name,b, c,crec (push_rel d env) (rea,reca))
       | [],[] -> mkExistential isevars env (dummy_loc, InternalHole)
       | _ -> anomaly "rec_branch_scheme"
   in 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e0eecf703..0960c2fda 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -217,7 +217,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
-	       let arg = process_pos env nF (lift 1 (body_of_type t)) in 
+	       let arg = process_pos env nF (lift 1 t) in 
                lambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
 		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 35c6a2370..3c746b49d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,7 +53,7 @@ let typeur sigma metamap =
            with Not_found -> anomaly "type_of: this is not a well-typed term")
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
-        lift n (body_of_type ty)
+        lift n ty
     | Var id ->
         (try
           let (_,_,ty) = lookup_named id env in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 05411c68d..9fc7dc976 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -106,7 +106,7 @@ let mkProd_or_LetIn (na,body,t) c =
 (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
 let mkProd_wo_LetIn (na,body,t) c =
   match body with
-    | None -> mkProd (na, body_of_type t, c)
+    | None -> mkProd (na,  t, c)
     | Some b -> subst1 b c
 
 let it_mkProd_wo_LetIn ~init = 
@@ -309,9 +309,9 @@ let occur_var env s c =
 
 let occur_var_in_decl env hyp (_,c,typ) =
   match c with
-    | None -> occur_var env hyp (body_of_type typ)
+    | None -> occur_var env hyp typ
     | Some body ->
-        occur_var env hyp (body_of_type typ) ||
+        occur_var env hyp typ ||
         occur_var env hyp body
 
 (* Tests that t is a subterm of c *)
@@ -542,7 +542,7 @@ let hdchar env c =
 	 else
 	   try match Environ.lookup_rel (n-k) env with
 	     | (Name id,_,_)   -> lowercase_first_char id
-	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) (body_of_type t))
+	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
 	   with Not_found -> "y")
     | Fix ((_,i),(lna,_,_)) -> 
 	let id = match lna.(i) with Name id -> id | _ -> assert false in
@@ -714,7 +714,7 @@ let assums_of_rel_context sign =
     (fun (na,c,t) l ->
       match c with
           Some _ -> l
-        | None -> (na,body_of_type t)::l)
+        | None -> (na, t)::l)
     sign ~init:[]
 
 let lift_rel_context n sign =
@@ -745,9 +745,9 @@ let make_all_name_different env =
 let global_vars env ids = Idset.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
-  | (_,None,t) -> global_vars_set env (body_of_type t)
+  | (_,None,t) -> global_vars_set env t
   | (_,Some c,t) ->
-      Idset.union (global_vars_set env (body_of_type t))
+      Idset.union (global_vars_set env t)
         (global_vars_set env c)
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)