diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-11-16 16:22:53 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-16 16:31:56 +0100 |
| commit | 37e0ce25f88a77c48c480e37ccca444a8f5fe4e8 (patch) | |
| tree | 040bcaeb51c7a1b13778c8d33e3332e8daa35ef5 /tactics/class_tactics.ml | |
| parent | 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a (diff) | |
Minor debug printing bug,
Hit by OCaml's "if then else" with no "end" once more
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4138562c6..e44ace425 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1318,10 +1318,9 @@ module Search = struct Feedback.msg_debug (str"Starting resolution with " ++ int i ++ str" goal(s) under focus and " ++ int (List.length initshelf) ++ str " shelved goal(s)" ++ - if only_classes then str " in only_classes mode" else - str " in regular mode" ++ - match depth with None -> str ", unbounded" - | Some i -> str ", with depth limit " ++ int i)); + (if only_classes then str " in only_classes mode" else str " in regular mode") ++ + match depth with None -> str ", unbounded" + | Some i -> str ", with depth limit " ++ int i)); tac let run_on_evars p evm tac = |