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

9 files changed, 24 insertions, 24 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 849ee225bb..f7c739fe6b 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 e0eecf7030..0960c2fda9 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 35c6a2370a..3c746b49dc 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 05411c68d2..9fc7dc9764 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 *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 08953ffe0d..9c65bdbbfe 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -230,7 +230,7 @@ let make_resolves env sigma name eap (c,cty) =
 let make_resolve_hyp env sigma (hname,_,htyp) = 
   try
     [make_apply_entry env sigma (true, false) hname
-       (mkVar hname, body_of_type htyp)]
+       (mkVar hname,  htyp)]
   with 
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
@@ -722,7 +722,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
-		hid (mkVar hid,body_of_type htyp)]
+		hid (mkVar hid, htyp)]
 	   with Failure _ -> [] 
 	 in
          search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d] g') 
@@ -819,7 +819,7 @@ let compileAutoArg contac = function
 	 tclFIRST 
            (List.map 
               (fun (id,_,typ) -> 
-                let cl = snd (decompose_prod (body_of_type typ)) in
+                let cl = snd (decompose_prod typ) in
                  if Hipattern.is_conjunction cl
 		 then 
 		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] 
@@ -845,7 +845,7 @@ let rec super_search n db_list local_db argl goal =
 	   let (hid,_,htyp) = pf_last_hyp g in
 	   let hintl =
 	     make_resolves (pf_env g) (project g)
-	       hid (true,false) (mkVar hid,body_of_type htyp) in
+	       hid (true,false) (mkVar hid, htyp) in
 	   super_search n db_list (Hint_db.add_list hintl local_db)
 	     argl g))
      ::
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 27eb73d0a1..55134310fa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -118,7 +118,7 @@ let pr_value env = function
      VContext _ | VFun _ | VRec _) -> str "<fun>"
 
 (* Transforms a named_context into a (string * constr) list *)
-let make_hyps = List.map (fun (id,_,typ) -> (id,body_of_type typ))
+let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
 
 (* Transforms an id into a constr if possible *)
 let constr_of_id ist id =
@@ -546,7 +546,7 @@ let rec glob_atomic lf ist = function
   | TacExtend (opn,l) ->
       let _ = lookup_tactic opn in
       TacExtend (opn,List.map (glob_genarg ist) l)
-  | TacAlias (_,l,body) -> failwith "TODO"
+  | TacAlias (_,l,body) -> failwith "TacAlias globalisation: TODO"
 
 and glob_tactic ist tac = snd (glob_tactic_seq ist tac)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 37da503fd8..62c95b53fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -396,8 +396,8 @@ let rec intros_move = function
 
 let dependent_in_decl a (_,c,t) =
   match c with
-    | None -> dependent a (body_of_type t)
-    | Some body -> dependent a body || dependent a (body_of_type t)
+    | None -> dependent a t
+    | Some body -> dependent a body || dependent a t
 
 let move_to_rhyp rhyp gl =
   let rec get_lhyp lastfixed depdecls = function
@@ -757,7 +757,7 @@ let (assumption : tactic) = fun gl ->
   let rec arec = function
     | [] -> error "No such assumption"
     | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl (body_of_type t) concl then refine (mkVar id) gl
+	if pf_conv_x_leq gl t concl then refine (mkVar id) gl
 	else arec rest
   in
   arec (pf_hyps gl)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 93277300b0..26cf3083cf 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -209,7 +209,7 @@ let process_object oldenv olddir full_olddir newdir
 	    match c with
 	      | None ->
 		  SectionLocalAssum
-		    (expmod_constr oldenv work_alist (body_of_type t))
+		    (expmod_constr oldenv work_alist t)
 	      | Some body ->
 		  SectionLocalDef
 		    (expmod_constr oldenv work_alist body)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 82991495d5..a64c3b800a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -169,12 +169,12 @@ let explain_cant_apply_not_functional ctx rator randl =
   let ctx = make_all_name_different ctx in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr = prterm_env ctx rator.uj_val in
-  let prt = prterm_env ctx (body_of_type rator.uj_type) in
+  let prt = prterm_env 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 = prterm_env ctx c.uj_val in
-		  let pct = prterm_env ctx (body_of_type c.uj_type) in
+		  let pct = prterm_env ctx c.uj_type in
 		  hov 2 (pc ++ spc () ++ str": "  ++ pct)) randl
   in
   str"Illegal application (Non-functional construction): " ++ 
@@ -248,7 +248,7 @@ let explain_ill_formed_rec_body ctx err names i vdefs =
 
 let explain_ill_typed_rec_body ctx i names vdefj vargs =
   let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
-  let pv = prterm_env ctx (body_of_type vargs.(i)) in
+  let pv = prterm_env 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 () ++