X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=210f3ed2f94fce78cabafea90cbfc825906c271a;hb=52af0e3a6ab827464f33b90bf0d39e5df3169499;hp=2224e56ef6fbbcbdbe32b3589dc2fb7ad2c92a1f;hpb=95977594b05ba0320784a445d480b3fe11ef4e55;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 2224e56ef..210f3ed2f 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -415,6 +415,27 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let ids_to_hypotheses = Hashtbl.create 23 in
     let hypotheses_seed = ref 0 in
     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
+    let sequent =
+     let i,canonical_context,term = sequent in
+      let canonical_context' =
+       List.fold_right
+        (fun d canonical_context' ->
+          let d' =
+           match d with
+              None -> None
+            | Some (n, Cic.Decl t)->
+               Some (n, Cic.Decl (Unshare.unshare t))
+            | Some (n, Cic.Def (t,None)) ->
+               Some (n,
+                Cic.Def ((Unshare.unshare t),None))
+            | Some (_,Cic.Def (_,Some _)) -> assert false
+          in
+           d::canonical_context'
+        ) [] canonical_context
+      in
+      let term' = Unshare.unshare term in
+       (i,canonical_context',term')
+    in
     let (metano,acontext,agoal) = 
       aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
       ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
@@ -505,46 +526,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