From 9e851246b1931372802ee54b0485b7d54dbe44d3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 7 Sep 2005 17:15:09 +0000 Subject: [PATCH] Unsharing bugs fixed. --- helm/ocaml/cic_omdoc/cic2acic.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index bc5405a9a..2c3b9fb62 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -426,12 +426,11 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = | 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 (n, Cic.Def ((Unshare.unshare t),None)) | Some (_,Cic.Def (_,Some _)) -> assert false in d::canonical_context' - ) [] canonical_context + ) canonical_context [] in let term' = Unshare.unshare term in (i,canonical_context',term') @@ -499,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)-> @@ -510,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') @@ -565,7 +564,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj = 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 (Unshare.unshare 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 -- 2.39.2