Eureka!

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

diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli
index 242b3102aa001f1a56f1f16e7451bf15b06fd68c..372f50085e317be663c75bb5ded0d88e0888955c 100644 (file)
--- a/helm/gTopLevel/oldDisambiguate.mli
+++ b/helm/gTopLevel/oldDisambiguate.mli
@@ -65,3 +65,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