Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / cic / deannotate.ml

diff --git a/helm/software/components/cic/deannotate.ml b/helm/software/components/cic/deannotate.ml
index b7c7d1113cdbd6fea17bb96ad90742b21436b3bc..f1dfbffed6614ef7c419bbe071d4fe1abde99ffa 100644 (file)
--- 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