X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.mli;h=b34d34342981c17c50436f97c2c12338bf63a71e;hb=30cbad3167cf714a8edc2dbc05c1fe8908e2542b;hp=479a5760c63f9fadb0906fdc498efeed31f8baf5;hpb=82466efd82082c6101d1c2c0c217f681b37160e8;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index 479a5760c..b34d34342 100644
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -23,21 +23,26 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented
 exception NotEnoughElements
 exception NameExpected
-exception Found of (Cic.name * Cic.context_entry) list
-exception NotImplemented
+
+val source_id_of_id : string -> string
+
+type anntypes =
+ {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
+;;
 
 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, Cic.annterm) Hashtbl.t ->      (* ids_to_inner_types *)
+  (Cic.id, anntypes) Hashtbl.t ->         (* ids_to_inner_types *)
   Cic.metasenv ->                         (* metasenv *)
   Cic.context ->                          (* context *)
+  Cic.id list ->                          (* idrefs *)
   Cic.term ->                             (* term *)
+  Cic.term option ->                      (* expected type *)
   Cic.annterm                             (* annotated term *)
 
 val acic_object_of_cic_object :
@@ -46,6 +51,6 @@ val acic_object_of_cic_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, Cic.annterm) Hashtbl.t *     (* ids_to_inner_types *)
+    (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 *)