X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.mli;h=2dd0a2f319652c0995b5230369ed582596df8aff;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=4f686da443ef71b1cc2a4a869aa855f4b3a71a80;hpb=2e062d07e358eb95f0dcbec8fcdfbc2a4fb9ae1f;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli
index 4f686da44..2dd0a2f31 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.mli
+++ b/helm/ocaml/cic_omdoc/cic2acic.mli
@@ -24,7 +24,6 @@
  *)
 
 exception NotEnoughElements
-exception NameExpected
 
 val source_id_of_id : string -> string
 
@@ -32,11 +31,17 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
+type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+
+val string_of_sort: sort_kind -> string
+val sort_of_string: string -> sort_kind
+val sort_of_sort: Cic.sort -> sort_kind
+
 val acic_of_cic_context' :
   int ref ->                              (* seed *)
   (Cic.id, Cic.term) Hashtbl.t ->         (* ids_to_terms *)
   (Cic.id, Cic.id option) Hashtbl.t ->    (* ids_to_father_ids *)
-  (Cic.id, string) Hashtbl.t ->           (* ids_to_inner_sorts *)
+  (Cic.id, sort_kind) Hashtbl.t ->        (* ids_to_inner_sorts *)
   (Cic.id, anntypes) Hashtbl.t ->         (* ids_to_inner_types *)
   Cic.metasenv ->                         (* metasenv *)
   Cic.context ->                          (* context *)
@@ -46,11 +51,12 @@ 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 *)
     (Cic.id, Cic.id option) Hashtbl.t *   (* ids_to_father_ids *)
-    (Cic.id, string) Hashtbl.t *          (* ids_to_inner_sorts *)
+    (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
     (Cic.id, anntypes) Hashtbl.t *        (* ids_to_inner_types *)
     (Cic.id, Cic.conjecture) Hashtbl.t *  (* ids_to_conjectures *)
     (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
@@ -61,5 +67,6 @@ val asequent_of_sequent :
     Cic.annconjecture *                   (* annotated conjecture *)
     (Cic.id, Cic.term) Hashtbl.t *        (* ids_to_terms *)
     (Cic.id, Cic.id option) Hashtbl.t *   (* ids_to_father_ids *)
-    (Cic.id, string) Hashtbl.t *          (* ids_to_inner_sorts *)
+    (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
     (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
+