aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/sos_lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/sos_lib.ml')
-rw-r--r--plugins/micromega/sos_lib.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index a9228365e..baf90d4da 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -606,16 +606,16 @@ let rec deepen f n =
exception TooDeep
-let deepen_until limit f n =
+let deepen_until limit f n =
match compare limit 0 with
| 0 -> raise TooDeep
| -1 -> deepen f n
- | _ ->
+ | _ ->
let rec d_until f n =
- try(* if !debugging
- then (print_string "Searching with depth limit ";
+ try(* if !debugging
+ then (print_string "Searching with depth limit ";
print_int n; print_newline()) ;*) f n
- with Failure x ->
+ with Failure x ->
(*if !debugging then (Printf.printf "solver error : %s\n" x) ; *)
if n = limit then raise TooDeep else d_until f (n + 1) in
d_until f n