]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2acic.mli
first moogle template checkin
[helm.git] / helm / ocaml / cic_omdoc / cic2acic.mli
index 4f686da443ef71b1cc2a4a869aa855f4b3a71a80..0288125b9a8ef6e64c17c6c85379346105d2b163 100644 (file)
@@ -24,7 +24,6 @@
  *)
 
 exception NotEnoughElements
-exception NameExpected
 
 val source_id_of_id : string -> string
 
@@ -46,6 +45,7 @@ val acic_of_cic_context' :
   Cic.annterm                             (* annotated term *)
 
 val acic_object_of_cic_object :
+  ?eta_fix: bool ->                       (* perform eta_fixing; default: true*)
   Cic.obj ->                              (* object *)
    Cic.annobj *                           (* annotated object *)
     (Cic.id, Cic.term) Hashtbl.t *        (* ids_to_terms *)