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

3 files changed, 9 insertions, 9 deletions

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)