* Abst removed from the DTD

[helm.git] / helm / gTopLevel / cic2acic.mli

diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index a2c0497f1e3658aebaa8dfa270ccae89b65de7bf..a07b9d2979b9f4f702d163a5cf4bfce4b3ae5d02 100644 (file)
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -27,15 +27,20 @@ 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.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 *)