X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=c5bbfff78b34d658e347e817d84c0857d8b0aae5;hb=0bfad3f438ba29135f2c18d1bf3cb0c8f462a205;hp=bb00476b97b73faf25e2fed68d891855c3a06aaf;hpb=07c5372510a5abecd788aa0b500e5deaa548c9d4;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index bb00476b9..c5bbfff78 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -300,20 +300,13 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
               C.ALambda
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
-          | C.LetIn (n,s,t) ->
-             let s_ty =
-              try
-               (cic_CicHash_find terms_to_types s).D.synthesized
-              with
-               Not_found ->
-                cicReduction_whd context (xxx_type_of_aux' metasenv context s);
-             in
+          | C.LetIn (n,s,ty,t) ->
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
                add_inner_type fresh_id'' ;
               C.ALetIn
-               (fresh_id'', n, aux' context idrefs s,
-                aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t)
+               (fresh_id'', n, aux' context idrefs s, aux' context idrefs ty,
+                aux' ((Some (n, C.Def(s,ty)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = `Prop then
@@ -429,12 +422,21 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            Hashtbl.add ids_to_hypotheses hid binding ;
            incr hypotheses_seed ;
            match binding with
-               Some (n,Cic.Def (t,_)) ->
-                 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
-                 Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
-                  (Some hid);
-                 (binding::context),
-                   ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
+               Some (n,Cic.Def (t,ty)) ->
+                 let acic =
+                  acic_of_cic_context ~computeinnertypes context idrefs t
+                   None in
+                 let acic2 =
+                  acic_of_cic_context ~computeinnertypes context idrefs ty
+                   None
+                 in
+                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
+                   (Some hid);
+                  Hashtbl.replace ids_to_father_ids
+                   (CicUtil.id_of_annterm acic2) (Some hid);
+                  (binding::context),
+                    ((hid,Some (n,Cic.ADef (acic,acic2)))::acontext),
+                    (hid::idrefs)
              | Some (n,Cic.Decl t) ->
                  let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
                  Hashtbl.replace ids_to_father_ids (CicUtil.id_of_annterm acic)
@@ -469,10 +471,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
               None -> None
             | 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 (bo,Some ty)) ->
-               Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
+            | Some (n,Cic.Def (bo,ty)) ->
+               Some (n, Cic.Def (Unshare.unshare bo,Unshare.unshare ty))
           in
            d::canonical_context'
         ) canonical_context []
@@ -549,10 +549,11 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
                    None -> None
                  | Some (n, C.Decl t)->
                     Some (n, C.Decl (eta_fix_and_unshare conjectures canonical_context' t))
-                 | Some (n, C.Def (t,None)) ->
+                 | Some (n, C.Def (t,ty)) ->
                     Some (n,
-                     C.Def ((eta_fix_and_unshare conjectures canonical_context' t),None))
-                 | Some (_,C.Def (_,Some _)) -> assert false
+                     C.Def
+                      (eta_fix_and_unshare conjectures canonical_context' t,
+                       eta_fix_and_unshare conjectures canonical_context' ty))
                in
                 d::canonical_context'
              ) canonical_context []
@@ -667,10 +668,10 @@ let plain_acic_term_of_cic_term =
        C.ALambda
         (fresh_id,n, aux context s,
          aux ((fresh_id, Some (n, C.Decl s))::context) t)
-   | C.LetIn (n,s,t) ->
+   | C.LetIn (n,s,ty,t) ->
       C.ALetIn
-       (fresh_id, n, aux context s,
-        aux ((fresh_id, Some (n, C.Def(s,None)))::context) t)
+       (fresh_id, n, aux context s, aux context ty,
+        aux ((fresh_id, Some (n, C.Def(s,ty)))::context) t)
    | C.Appl l ->
       C.AAppl (fresh_id, List.map (aux context) l)
    | C.Const (uri,exp_named_subst) ->