]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/disambiguation/disambiguateTypes.mli
diamond property
[helm.git] / matitaB / components / disambiguation / disambiguateTypes.mli
index 1e99fd404ace0ebfad221082340ed3b98365b144..5ebc835cb4ac3ca9602ae7db3cfab7070a538aa0 100644 (file)
  *)
 
 type domain_item =
- | Id of string               (* literal *)
- | Symbol of string * int     (* literal, instance num *)
- | Num of int                 (* instance num *)
+ | Id of (string * string option)              (* literal, opt. uri *)
+ | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
+ | Num of (string option * string) option             (* opt. uri, interpretation *)
 
 (* module Domain:      Set.S with type elt = domain_item *)
 module Environment:
 sig
-  include Map.S with type key = domain_item
+  include Map.S with type key = domain_item 
   val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t
 end