summaryrefslogtreecommitdiff
path: root/lib/explore.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /lib/explore.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'lib/explore.mli')
-rw-r--r--lib/explore.mli10
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/explore.mli b/lib/explore.mli
index 07f95e8a..e29f2795 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -6,18 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: explore.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
(*s Search strategies. *)
(*s A search problem implements the following signature [SearchProblem].
[state] is the type of states of the search tree.
- [branching] is the branching function; if [branching s] returns an
+ [branching] is the branching function; if [branching s] returns an
empty list, then search from [s] is aborted; successors of [s] are
recursively searched in the order they appear in the list.
- [success] determines whether a given state is a success.
+ [success] determines whether a given state is a success.
- [pp] is a pretty-printer for states used in debugging versions of the
+ [pp] is a pretty-printer for states used in debugging versions of the
search functions. *)
module type SearchProblem = sig
@@ -33,7 +33,7 @@ module type SearchProblem = sig
end
(*s Functor [Make] returns some search functions given a search problem.
- Search functions raise [Not_found] if no success is found.
+ Search functions raise [Not_found] if no success is found.
States are always visited in the order they appear in the
output of [branching] (whatever the search method is).
Debugging versions of the search functions print the position of the