X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaTypes.ml;h=95618d142624e932493666da151773b8d9f412c5;hb=db8cb29c71b8a7203e1038223e39cfc349671aa7;hp=a9e74bf5fdbf1e0bef21d76681dc61481454a85d;hpb=642e20a0135126586603ffb539f0d1c1428f1502;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index a9e74bf5f..95618d142 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -75,6 +75,8 @@ class type console =
     method echo_error     : string -> unit
     method clear          : unit -> unit
     method wrap_exn       : 'a. (unit -> 'a) -> 'a option
+    method choose_uri     : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 type choose_uris_callback =
@@ -158,7 +160,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]