diff options
| author | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
| commit | 5360ec8ff56c44e96c56965be78e6f2538963a57 (patch) | |
| tree | 82361651080323e8ab33db31890c32b93f6928ea /tactics | |
| parent | 5ea95f9cd843bec4504646851bf22bf505e56ad8 (diff) | |
| parent | 9ddfdab6a4715a08a78296bf8824d086f358bdc0 (diff) | |
Merge PR#636: Miscellaneous typos, dead code, etc.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd23..05eb0a9760 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,7 +1202,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ Printer.pr_econstr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ + str ", " ++ int (List.length poss) ++ str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx |