From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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