X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=0cfd8f07cfe620ed9e2fe58438b6c7d97744b5c6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9292ece0b839d2a0b1952400b06b7f1916e2b9c0;hpb=96c2feeb6b1d27e25b7bca582ff6c25a4f87dca8;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 9292ece0b..0cfd8f07c 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -41,7 +41,7 @@ let get_current_status_as_xml () =
       let uri = match uri with Some uri -> uri | None -> assert false in
       let currentproof =
        (*CSC: Wrong: [] is just plainly wrong *)
-       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
+       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])
       in
        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof