X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FoldDisambiguate.mli;h=8fcc1c9341544e64390ed6ecd8e85d7b2d6c6796;hb=98295941bee765a0cb4070eb3f2df553228c11c8;hp=242b3102aa001f1a56f1f16e7451bf15b06fd68c;hpb=12809955a4a6c693072f5b924603165f83cc382e;p=helm.git

diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli
index 242b3102a..8fcc1c934 100644
--- a/helm/gTopLevel/oldDisambiguate.mli
+++ b/helm/gTopLevel/oldDisambiguate.mli
@@ -38,7 +38,6 @@
 
 module type Callbacks =
   sig
-    val output_html : ?append_NL:bool -> Ui_logger.html_msg -> unit
     val interactive_user_uri_choice :
       selection_mode:[`SINGLE | `MULTIPLE] ->
       ?ok:string ->
@@ -65,3 +64,11 @@ module Make (C : Callbacks) :
         id_to_uris:domain_and_interpretation ->
         domain_and_interpretation * Cic.metasenv * Cic.term
     end
+
+module EnvironmentP3 :
+ sig
+  type t = domain_and_interpretation
+  val empty : string
+  val to_string : t -> string
+  val of_string : string -> t
+ end