From c31fabdc5aadbf22d1d27f22aa737188acc6f12b Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 27 Aug 2007 11:41:08 +0000 Subject: 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 --- contrib/xml/xmlcommand.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'contrib/xml/xmlcommand.ml') 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 -- cgit v1.2.3