Added flag ?eta_fix:bool to acic_object_of_cic_object.

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index a9199c0e880f07b061a65d9b8655c334ec21eb6f..1077f15c2bc6a03cdaa7b2c9cd6b854c857446a5 100644 (file)
--- 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