Suppression des type_app et body_of_type qui alourdissent inutilement le code

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

3 files changed, 8 insertions, 10 deletions

diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 8a5967a23c..75e428e14d 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -241,16 +241,15 @@ let typeur sigma metamap =
     | T.Var id ->
         (try
           let (_,_,ty) = Environ.lookup_named id env in
-          T.body_of_type ty
+          ty
         with Not_found ->
           Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
     | T.Evar ev -> Evd.existential_type sigma ev
-    | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
-    | T.Construct cstr ->
-       T.body_of_type (Inductiveops.type_of_constructor env cstr)
+    | T.Ind ind -> Inductiveops.type_of_inductive env ind
+    | T.Construct cstr -> Inductiveops.type_of_constructor env cstr
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index cce788912d..de8c540caf 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -51,7 +51,7 @@ let type_judgment env sigma j =
 ;;
 
 let type_judgment_cprop env sigma j =
-  match Term.kind_of_term(whd_betadeltaiotacprop env sigma (Term.body_of_type j.Environ.uj_type)) with
+  match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with
     | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s }
     | _ -> None  (* None means the CProp constant *)
 ;;
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 0127132399..1aabd4348e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -329,14 +329,13 @@ let mk_variable_obj id body typ =
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.string_of_id id, unsharedbody,
-     (Unshare.unshare (Term.body_of_type typ)), params)
+    (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 (* Unsharing is not performed on the body, that must be already unshared. *)
 (* The evar map and the type, instead, are unshared by this function.     *)
 let mk_current_proof_obj is_a_variable id bo ty evar_map env =
- let unshared_ty = Unshare.unshare (Term.body_of_type ty) in
+ let unshared_ty = Unshare.unshare ty in
  let metasenv =
   List.map
    (function
@@ -384,7 +383,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
 
 let mk_constant_obj id bo ty variables hyps =
  let hyps = string_list_of_named_context_list hyps in
- let ty = Unshare.unshare (Term.body_of_type ty) in
+ let ty = Unshare.unshare ty in
  let params = filter_params variables hyps in
   match bo with
      None ->
@@ -413,7 +412,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
           (Array.mapi
-           (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames)
+           (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
           []
          )
         in