Merge PR#636: Miscellaneous typos, dead code, etc.

7 files changed, 5 insertions, 16 deletions

diff --git a/CHANGES b/CHANGES
index 8cb5573b21..69271f932e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,13 +17,12 @@ Tactics
     Most notably, the new implementation recognizes Miller patterns that were
     missed before because of a missing normalization step. Hopefully this should
     be fairly uncommon.
-- "auto with real" can now discharge comparisons of literals
+- Tactic "auto with real" can now discharge comparisons of literals.
 - The types of variables in patterns of "match" are now
   beta-iota-reduced after type-checking. This has an impact on the
   type of the variables that the tactic "refine" introduces in the
   context, producing types a priori closer to the expectations.
 
-
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c0..b57a046796 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -900,7 +900,7 @@ let interp_reference vars r =
 (**********************************************************************)
 (** {5 Cases }                                                        *)
 
-(** {6 Elemtary bricks } *)
+(** {6 Elementary bricks } *)
 let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fc9d70ae7d..c649cfb2c6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -8,7 +8,7 @@
 
 (* The `Quote' tactic *)
 
-(* The basic idea is to automatize the inversion of interpetation functions
+(* The basic idea is to automatize the inversion of interpretation functions
    in 2-level approach
 
    Examples are given in \texttt{theories/DEMOS/DemoQuote.v}
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/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebdae..93b25e2ede 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -544,13 +544,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir =
 let add_rec_dir_import add_file phys_dir log_dir =
   add_directory true (add_file true) phys_dir log_dir
 
-(** -R semantic but only on immediate capitalized subdirs *)
-
-let add_rec_uppercase_subdirs add_file phys_dir log_dir =
-  process_subdirectories (fun phys_dir f ->
-    add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
-    phys_dir
-
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
   add_directory false add_caml_known phys_dir []
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 633c474ada..10da0240dd 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -64,8 +64,5 @@ val add_rec_dir_no_import :
 val add_rec_dir_import :
   (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
 
-val add_rec_uppercase_subdirs :
-  (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-
 val treat_file : dir -> string -> unit
 val error_cannot_parse : string -> int * int -> 'a
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