aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2d6dffdd2..05eb0a976 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