Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic / deannotate.ml

diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml
index df59305fea29d1af45a52dc3f771234775e94448..2bee18d6f161e3c82c88c0e1d64fcd7f64df5204 100644 (file)
--- a/helm/ocaml/cic/deannotate.ml
+++ b/helm/ocaml/cic/deannotate.ml
@@ -108,7 +108,7 @@ let deannotate_obj =
             List.map 
              (function 
                  _,Some (n,(C.ADef at)) ->
-                   Some (n,(C.Def (deannotate_term at)))
+                   Some (n,(C.Def ((deannotate_term at),None)))
                | _,Some (n,(C.ADecl at)) ->
                    Some (n,(C.Decl (deannotate_term at)))
                | _,None -> None