aboutsummaryrefslogtreecommitdiff
path: root/lib/dnet.mli
diff options
context:
space:
mode:
authorglondu2009-09-17 15:58:14 +0000
committerglondu2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /lib/dnet.mli
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/dnet.mli')
-rw-r--r--lib/dnet.mli18
1 files changed, 9 insertions, 9 deletions
diff --git a/lib/dnet.mli b/lib/dnet.mli
index a01bbb0e2e..b2f2714720 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.mli
@@ -33,7 +33,7 @@
symmetric, see term_dnet.ml).
The complexity of the search is (almost) the depth of the term.
-
+
To use it, you have to provide a module (Datatype) with the datatype
parametrized on the recursive argument. example:
@@ -70,13 +70,13 @@ end
module type S =
sig
type t
-
+
(* provided identifier type *)
type ident
(* provided metavariable type *)
type meta
-
+
(* provided parametrized datastructure *)
type 'a structure
@@ -92,13 +92,13 @@ sig
type term_pattern = 'a structure pattern as 'a
val empty : t
-
+
(* [add t w i] adds a new association (w,i) in t. *)
val add : t -> term_pattern -> ident -> t
-
+
(* [find_all t] returns all identifiers contained in t. *)
val find_all : t -> Idset.t
-
+
(* [fold_pattern f acc p dn] folds f on each meta of p, passing the
meta and the sub-dnet under it. The result includes:
- Some set if identifiers were gathered on the leafs of the term
@@ -118,10 +118,10 @@ sig
(* apply a function on each identifier and node of terms in a dnet *)
val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
end
-
+
module Make :
- functor (T:Datatype) ->
- functor (Ident:Set.OrderedType) ->
+ functor (T:Datatype) ->
+ functor (Ident:Set.OrderedType) ->
functor (Meta:Set.OrderedType) ->
S with type ident = Ident.t
and type meta = Meta.t