Added flag ?eta_fix:bool to acic_object_of_cic_object.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index b62f4b6245dbc5b88b73df47bc8ab77633277f49..03d12a4c5150057c475785775d702a3b873b1ab5 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -478,7 +478,7 @@ let save_obj uri obj =
   (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
    ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
  =
-  Cic2acic.acic_object_of_cic_object obj
+  Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
  in
   (* let's save the theorem and register it to the getter *) 
   let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in