From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 08:35:34 +0000 (+0000) Subject: Dead code removed. X-Git-Tag: V_0_1_2_1~88 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c61dbec2286f7a39a88c30d657947b2b144ca4a;p=helm.git Dead code removed. --- diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 2224e56ef..9c62ae845 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -505,46 +505,6 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = = aconjecture_of_conjecture' conjectures conjecture in (cid,i,acanonical_context,aterm)) conjectures' in -(* let idrefs',revacanonical_context = - let rec aux context idrefs = - function - [] -> idrefs,[] - | hyp::tl -> - let hid = "h" ^ string_of_int !hypotheses_seed in - let new_idrefs = hid::idrefs in - xxx_add ids_to_hypotheses hid hyp ; - incr hypotheses_seed ; - match hyp with - (Some (n,C.Decl t)) -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl in - let at = - acic_term_of_cic_term_context' - conjectures context idrefs t None - in - final_idrefs,(hid,Some (n,C.ADecl at))::atl - | (Some (n,C.Def (t,_))) -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl in - let at = - acic_term_of_cic_term_context' - conjectures context idrefs t None - in - final_idrefs,(hid,Some (n,C.ADef at))::atl - | None -> - let final_idrefs,atl = - aux (hyp::context) new_idrefs tl - in - final_idrefs,(hid,None)::atl - in - aux [] [] (List.rev canonical_context) - in - let aterm = - acic_term_of_cic_term_context' conjectures - canonical_context idrefs' term None - in - (cid,i,(List.rev revacanonical_context),aterm) - ) conjectures' in *) (* let time1 = Sys.time () in *) let bo' = eta_fix conjectures' [] bo in let ty' = eta_fix conjectures' [] ty in