X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fdeannotate.ml;h=f1dfbffed6614ef7c419bbe071d4fe1abde99ffa;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=b7c7d1113cdbd6fea17bb96ad90742b21436b3bc;hpb=66929b8edb58d468a134b648466f3e9c45ba5c0e;p=helm.git

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index b7c7d1113..f1dfbffed 100644
--- a/helm/software/components/cic/deannotate.ml
+++ b/helm/software/components/cic/deannotate.ml
@@ -51,8 +51,8 @@ let rec deannotate_term =
       C.Prod (name, deannotate_term so, deannotate_term ta)
    | C.ALambda (_,name,so,ta) ->
       C.Lambda (name, deannotate_term so, deannotate_term ta)
-   | C.ALetIn (_,name,so,ta) ->
-      C.LetIn (name, deannotate_term so, deannotate_term ta)
+   | C.ALetIn (_,name,so,ty,ta) ->
+      C.LetIn (name, deannotate_term so, deannotate_term ty, deannotate_term ta)
    | C.AAppl (_,l) -> C.Appl (List.map deannotate_term l)
    | C.AConst (_,uri,exp_named_subst) ->
       let deann_exp_named_subst =
@@ -97,7 +97,8 @@ let deannotate_conjectures =
       let context = 
        List.map 
         (function 
-          | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None)))
+          | _,Some (n,(C.ADef (ate,aty))) ->
+             Some(n,(C.Def(deannotate_term ate,deannotate_term aty)))
           | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
           | _,None -> None)
         acontext