diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /lib/explore.ml | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/explore.ml')
| -rw-r--r-- | lib/explore.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/explore.ml b/lib/explore.ml index 31a96774..3d57fc08 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -21,7 +21,7 @@ module Make = functor(S : SearchProblem) -> struct type position = int list - let msg_with_position p pp = + let msg_with_position (p : position) pp = let rec pp_rec = function | [] -> mt () | [i] -> int i @@ -50,7 +50,7 @@ module Make = functor(S : SearchProblem) -> struct in explore [1] s - (*s Breadth first search. We use functional FIFOS à la Okasaki. *) + (*s Breadth first search. We use functional FIFOS Ã la Okasaki. *) type 'a queue = 'a list * 'a list @@ -58,7 +58,7 @@ module Make = functor(S : SearchProblem) -> struct let empty = [],[] - let push x (h,t) = (x::h,t) + let push x (h,t) : _ queue = (x::h,t) let pop = function | h, x::t -> x, (h,t) |