From 95977594b05ba0320784a445d480b3fe11ef4e55 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 12:58:23 +0000 Subject: [PATCH] Unsharing finally introduced (but just for object processing, not yet for terms and sequents). --- helm/ocaml/cic_omdoc/cic2acic.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) 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 ;; - - -- 2.39.2