new logger

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

diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli
index 242b3102aa001f1a56f1f16e7451bf15b06fd68c..8fcc1c9341544e64390ed6ecd8e85d7b2d6c6796 100644 (file)
--- 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