Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

6 files changed, 12 insertions, 20 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c8c75cd5e..3e26eb9a7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -905,9 +905,7 @@ let rec super_search n db_list local_db argl goal =
 let search_superauto n ids argl g = 
   let sigma =
     List.fold_right
-      (fun id -> add_named_assum
-	   (id,Retyping.get_assumption_of (pf_env g) (project g) 
-	      (pf_type_of g (pf_global g id))))
+      (fun id -> add_named_assum (id, pf_type_of g (pf_global g id)))
       ids empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9efdd718e..74f7bf2f2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -128,13 +128,11 @@ let rec add_prods_sign env sigma t =
     | IsProd (na,c1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-	let j = Retyping.get_assumption_of env sigma c1 in
-        add_prods_sign (Environ.push_named_assum (id,j) env) sigma b'
+        add_prods_sign (Environ.push_named_assum (id,c1) env) sigma b'
     | IsLetIn (na,c1,t1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-	let j = Retyping.get_assumption_of env sigma t1 in
-        add_prods_sign (Environ.push_named_def (id,c1,j) env) sigma b'
+        add_prods_sign (Environ.push_named_def (id,c1,t1) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -176,8 +174,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let nptyj = make_typed npty (Retyping.get_sort_of env sigma npty) in
-  let extenv = push_named_assum (p,nptyj) env in
+  let extenv = push_named_assum (p,npty) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
diff --git a/tactics/refine.ml b/tactics/refine.ml
index faa49b3e2..904ed3038 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -138,8 +138,7 @@ let rec compute_metamap env c = match kind_of_term c with
    *    où x est une variable FRAICHE *)
   | IsLambda (name,c1,c2) ->
       let v = fresh env name in
-      let tj = Retyping.get_assumption_of env Evd.empty c1 in
-      let env' = push_named_assum (v,tj) env in
+      let env' = push_named_assum (v,c1) env in
       begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -179,9 +178,7 @@ let rec compute_metamap env c = match kind_of_term c with
   | IsFix ((ni,i),(ai,fi,v)) ->
       let vi = List.rev (List.map (fresh env) fi) in
       let env' =
-	List.fold_left
-	  (fun env (v,ar) -> push_named_assum (v,Retyping.get_assumption_of env Evd.empty ar) env)
-	  env
+	List.fold_left (fun env (v,ar) -> push_named_assum (v, ar) env) env
 	  (List.combine vi (Array.to_list ai)) 
       in
       let a = Array.map
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 6f7499057..2a6ddcbac 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1717,9 +1717,9 @@ let rec lisvarprop = function
 let rec constr_lseq gls = function
   | [] -> []
   | (idx,c,hx)::rest -> 
-      match Retyping.get_sort_of (pf_env gls) (project gls) (incast_type hx) with
+      match Retyping.get_sort_of (pf_env gls) (project gls) hx with
         | Prop Null -> 
-            (TVar(string_of_id idx),tauto_of_cci_fmla gls (body_of_type hx))
+            (TVar(string_of_id idx),tauto_of_cci_fmla gls hx)
             :: constr_lseq gls rest
         |_-> constr_lseq gls rest
 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 4943756e3..ab046025f 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -93,9 +93,9 @@ let clenv_constrain_with_bindings bl clause =
 let add_prod_rel sigma (t,env) =
   match kind_of_term t with
     | IsProd (na,t1,b) ->
-        (b,push_rel_assum (na,Retyping.get_assumption_of env sigma t1) env)
+        (b,push_rel_assum (na, t1) env)
     | IsLetIn (na,c1,t1,b) ->
-        (b,push_rel_def (na,c1,Retyping.get_assumption_of env sigma t1) env)
+        (b,push_rel_def (na,c1, t1) env)
     | _ -> failwith "add_prod_rel"
 
 let rec add_prods_rel sigma (t,env) =
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index af96177b3..b3d372f21 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -33,10 +33,10 @@ val add_prods_rel : 'a evar_map -> constr * env -> constr * env
 
 (*i**
 val add_prod_sign : 
-  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+  'a evar_map -> constr * types signature -> constr * types signature
 
 val add_prods_sign : 
-  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+  'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
 val res_pf_THEN :