diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /lib/dnet.mli | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (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.mli | 18 |
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 |
