X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=fdc2cea1cee300573c739dfe597ea46896c52242;hb=7df065750ec593fb409ae8627f81927397602b9b;hp=bf80a5939b47153dd938a84f4a4e2ca96ef65127;hpb=f47b833df94d134090a65653077744290438a875;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index bf80a5939..fdc2cea1c 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -227,7 +227,7 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
       (match metasenv with
           None ->
            Cic.Constant
-            (id, Some (proof2cic deannotate bo), deannotate ty, params)
+            (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
         | Some metasenv' ->
            let metasenv'' =
             List.map
@@ -259,7 +259,8 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
              ) metasenv'
            in
             Cic.CurrentProof
-             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+              []))
   | _ -> raise ToDo
 ;;