diff options
| -rw-r--r-- | lib/dnet.ml | 14 | ||||
| -rw-r--r-- | lib/dnet.mli | 6 |
2 files changed, 8 insertions, 12 deletions
diff --git a/lib/dnet.ml b/lib/dnet.ml index a9e1e97e36..22ca7e78d1 100644 --- a/lib/dnet.ml +++ b/lib/dnet.ml @@ -27,10 +27,9 @@ sig type meta type 'a structure module Idset : Set.S with type elt=ident - type 'a pattern = - | Term of 'a + type term_pattern = + | Term of term_pattern structure | Meta of meta - type term_pattern = ('a structure) pattern as 'a val empty : t val add : t -> term_pattern -> ident -> t val find_all : t -> Idset.t @@ -51,18 +50,17 @@ struct type ident = Ident.t type meta = Meta.t - type 'a pattern = - | Term of 'a - | Meta of meta - type 'a structure = 'a T.t + type term_pattern = + | Term of term_pattern structure + | Meta of meta + module Idset = Set.Make(Ident) module Mmap = Map.Make(Meta) module Tmap = Map.Make(struct type t = unit structure let compare = T.compare end) - type term_pattern = term_pattern structure pattern type idset = Idset.t diff --git a/lib/dnet.mli b/lib/dnet.mli index 7ce43bd564..d2373a0d68 100644 --- a/lib/dnet.mli +++ b/lib/dnet.mli @@ -83,12 +83,10 @@ sig (** a pattern is a term where each node can be a unification variable *) - type 'a pattern = - | Term of 'a + type term_pattern = + | Term of term_pattern structure | Meta of meta - type term_pattern = 'a structure pattern as 'a - val empty : t (** [add t w i] adds a new association (w,i) in t. *) |