From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Sep 2005 17:15:09 +0000 (+0000)
Subject: Unsharing bugs fixed.
X-Git-Tag: V_0_1_2_1~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e851246b1931372802ee54b0485b7d54dbe44d3;p=helm.git

Unsharing bugs fixed.
---

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