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

1 files changed, 4 insertions, 5 deletions

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