X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.mli;h=0cd607bb67888aaa05fe472c49f8af0a9da53e91;hb=9f694d4bf47c7772dda4827f1b46f42cb435ec36;hp=a2c0497f1e3658aebaa8dfa270ccae89b65de7bf;hpb=cedc0cfe0ea81f94ac8b88b71d8f855a33329593;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index a2c0497f1..0cd607bb6 100644
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -23,19 +23,24 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented
 exception NotEnoughElements
 exception NameExpected
 
+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 :
@@ -44,6 +49,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 *)