aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/explore.mli
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /lib/explore.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/explore.mli')
-rw-r--r--lib/explore.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/explore.mli b/lib/explore.mli
index 907e2f256..e29f27955 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -12,12 +12,12 @@
(*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