X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=2c3b9fb629c294e6e9ab3658db3a400cb38c909b;hb=33dd8006a7e0eb9c6c2a93b4d98c8ef88d2d49d1;hp=608f6d7c3aa8af0faf616c448a2f693bb75de074;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 608f6d7c3..2c3b9fb62 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -415,6 +415,26 @@ 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
@@ -443,8 +463,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
     ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types 
     ids_to_hypotheses hypotheses_seed in 
    let eta_fix metasenv context t =
-    if eta_fix then E.eta_fix metasenv context t else t
-   in
+    let t = if eta_fix then E.eta_fix metasenv context t else t in
+     Unshare.unshare t in
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
@@ -478,7 +498,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
            let canonical_context' =
             List.fold_right
              (fun d canonical_context' ->
-               let d' =
+               let d =
                 match d with
                    None -> None
                  | Some (n, C.Decl t)->
@@ -489,7 +509,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
                  | Some (_,C.Def (_,Some _)) -> assert false
                in
                 d::canonical_context'
-             ) [] canonical_context
+             ) canonical_context []
            in
            let term' = eta_fix conjectures canonical_context' term in
             (i,canonical_context',term')
@@ -505,46 +525,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
@@ -577,9 +557,15 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
     | C.InductiveDefinition (tys,params,paramsno,attrs) ->
+       let tys =
+        List.map
+         (fun (name,i,arity,cl) ->
+           (name,i,Unshare.unshare arity,
+             List.map (fun (name,ty) -> name,Unshare.unshare ty) cl)) tys in
        let context =
         List.map
-         (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
+         (fun (name,_,arity,_) ->
+           Some (C.Name name, C.Decl (Unshare.unshare arity))) tys in
        let idrefs = List.map (function _ -> gen_id seed) tys in
        let atys =
         List.map2
@@ -599,5 +585,3 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses
 ;;
-
-