]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/testlibrary.ml
Added flag ?eta_fix:bool to acic_object_of_cic_object.
[helm.git] / helm / gTopLevel / testlibrary.ml
index 90563a6186ec078dc9d34252c8372ad6aa59b9be..21173e9e5308221a81ddb53841c44a0ba2827e9e 100644 (file)
@@ -35,7 +35,7 @@ let debug_print s = prerr_endline ("^^^^^^ " ^ s)
 let test_uri uri =
   let obj = CicCache.get_obj uri in
   let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
-    Cic2acic.acic_object_of_cic_object obj
+    Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
   in
   let ids_to_uris = Hashtbl.create 1023 in
   let round_trip annterm =