diff options
author | 2012-10-06 10:08:37 +0000 | |
---|---|---|
committer | 2012-10-06 10:08:37 +0000 | |
commit | f44b80f4b3e512d21653a019583e97b672b55010 (patch) | |
tree | 7587d6ac6ecfaaaca4afa926cd161d64fb9c1cae /lib/dnet.ml | |
parent | d1b3a5a52f1021e833c817aee17546095563abb6 (diff) |
avoid using rectypes in dnet.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/dnet.ml')
-rw-r--r-- | lib/dnet.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/lib/dnet.ml b/lib/dnet.ml index a9e1e97e3..22ca7e78d 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 |