added persit-file-implementation.

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

diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index a07b9d2979b9f4f702d163a5cf4bfce4b3ae5d02..b34d34342981c17c50436f97c2c12338bf63a71e 100644 (file)
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -23,10 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented
 exception NotEnoughElements
 exception NameExpected
 
+val source_id_of_id : string -> string
+
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
@@ -39,6 +40,7 @@ val acic_of_cic_context' :
   (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 *)