Yet another implementation of the single aliases / multi aliases idea.

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 5de2e5759eaa6c2a68ce3da74b746e2e7241db7a..87e09daef7705cf3f9331a6073d3ea5fe332f0c5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -32,9 +32,6 @@ val interpretate_path :
   context:Cic.name list -> DisambiguateTypes.term ->
     Cic.term
 
-  (** @param multi true if multi aliases are used, false otherwise *)
-type aliases = bool * DisambiguateTypes.environment
-
 module type Disambiguator =
 sig
   (** @param fresh_instances when set to true fresh instances will be generated
@@ -46,7 +43,8 @@ sig
     context:Cic.context ->
     metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:aliases ->               (* previous interpretation status *)
+    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:DisambiguateTypes.multiple_environment option ->
     DisambiguateTypes.term ->
     (DisambiguateTypes.environment * (* new interpretation status *)
      Cic.metasenv *                  (* new metasenv *)
@@ -58,7 +56,8 @@ sig
   val disambiguate_obj :
     ?fresh_instances:bool ->
     dbd:Mysql.dbd ->
-    aliases:aliases ->               (* previous interpretation status *)
+    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     GrafiteAst.obj ->
     (DisambiguateTypes.environment * (* new interpretation status *)