avoid using rectypes in dnet.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 12 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
 
 
diff --git a/lib/dnet.mli b/lib/dnet.mli
index 7ce43bd56..d2373a0d6 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. *)