diff options
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) |