Unsharing finally introduced (but just for object processing, not yet for terms

and sequents).

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 608f6d7c3aa8af0faf616c448a2f693bb75de074..2224e56ef6fbbcbdbe32b3589dc2fb7ad2c92a1f 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -443,8 +443,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) ->
@@ -577,9 +577,14 @@ 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 +604,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
 ;;
-
-