From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 12:58:23 +0000 (+0000) Subject: Unsharing finally introduced (but just for object processing, not yet for terms X-Git-Tag: V_0_1_2_1~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95977594b05ba0320784a445d480b3fe11ef4e55;p=helm.git 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 608f6d7c3..2224e56ef 100644 --- 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 ;; - -