X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=1077f15c2bc6a03cdaa7b2c9cd6b854c857446a5;hb=9f60b3b0f4460aec52ec241037f6c475b421dd15;hp=f320f08379d78a5c33f94ca1ac807bd4f7e5e650;hpb=f8d58fcacc3544aeabec15d2157cb5ef6e8d6840;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index f320f0837..1077f15c2 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -43,7 +43,7 @@ let get_current_status_as_xml () =
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
       in
        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
-        Cic2acic.acic_object_of_cic_object currentproof
+        Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
        in
         let xml, bodyxml =
          match
@@ -83,7 +83,7 @@ let metas_in_term term =
       C.Rel _ -> []
     | C.Meta (n,_) -> [n]
     | C.Sort _
-    | C.Implicit -> []
+    | C.Implicit _ -> []
     | C.Cast (te,ty) -> (aux te) @ (aux ty)
     | C.Prod (_,s,t) -> (aux s) @ (aux t)
     | C.Lambda (_,s,t) -> (aux s) @ (aux t)