Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

[helm.git] / matita / components / disambiguation / disambiguateTypes.mli

diff --git a/matita/components/disambiguation/disambiguateTypes.mli b/matita/components/disambiguation/disambiguateTypes.mli
index c3601eae5858c81ca9451667738a08329290972a..ef24e2ce8879be688a45c03df279ce660c98ad91 100644 (file)
--- a/matita/components/disambiguation/disambiguateTypes.mli
+++ b/matita/components/disambiguation/disambiguateTypes.mli
@@ -23,6 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
+type 'a expected_type = [ `XTNone       (* unknown *)
+                        | `XTSome of 'a (* the given term *) 
+                       | `XTSort       (* any sort *)
+                       | `XTInd        (* any (co)inductive type *)
+                        ]
+
 type domain_item =
  | Id of string               (* literal *)
  | Symbol of string * int     (* literal, instance num *)
@@ -48,13 +54,13 @@ type interactive_user_uri_choice_type =
   selection_mode:[`SINGLE | `MULTIPLE] ->
   ?ok:string ->
   ?enable_button_for_non_vars:bool ->
-  title:string -> msg:string -> id:string -> UriManager.uri list ->
-   UriManager.uri list
+  title:string -> msg:string -> id:string -> NReference.reference list ->
+   NReference.reference list
 
 type interactive_interpretation_choice_type = string -> int ->
   (Stdpp.location list * string * string) list list -> int list
 
 type input_or_locate_uri_type = 
-  title:string -> ?id:string -> unit -> UriManager.uri option
+  title:string -> ?id:string -> unit -> NReference.reference option
 
 val string_of_domain_item: domain_item -> string