debian version 0.0.5-6

[helm.git] / helm / matita / matitaTypes.mli

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 538b4b3243406b36039db5b9e7b46e227b0a738e..26299967224cb6b4f850da5a53935360691296e9 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -72,6 +72,8 @@ class type console =
     method echo_error : string -> unit
     method echo_message : string -> unit
     method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 class type disambiguator =
@@ -196,7 +198,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]