]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaTypes.ml
debian: rebuilt against ocaml 3.08.2
[helm.git] / helm / matita / matitaTypes.ml
index a9e74bf5fdbf1e0bef21d76681dc61481454a85d..95618d142624e932493666da151773b8d9f412c5 100644 (file)
@@ -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
   ]