From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 Aug 2016 14:46:33 +0200
Subject: Uniformity of style for selecting plural or not; spacing for comma.

---
 tactics/class_tactics.ml | 2 +-
 vernac/obligations.ml    | 2 +-
 2 files changed, 2 insertions(+), 2 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
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0520216b2..5233fab151 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
-- 
cgit v1.2.3