Merge PR#716: Don't double up on periods in anomalies

5 files changed, 7 insertions, 7 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6b046919d..902985827 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -536,7 +536,7 @@ type 'a extra_genarg_printer =
       hv 0
         (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
            prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
-    | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+    | [] -> anomaly (Pp.str "LetIn must declare at least one binding.")
 
   let pr_seq_body pr tl =
     hv 0 (str "[ " ++
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 3ff7b53c7..b237e917d 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -113,7 +113,7 @@ let rec to_ltacprof_tactic m xml =
          children = List.fold_left to_ltacprof_tactic M.empty xs;
        } in
       M.add name node m
-  | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML")
+  | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.")
 
 let to_ltacprof_results xml =
   let open Xml_datatype in
@@ -125,7 +125,7 @@ let to_ltacprof_results xml =
        max_total = 0.0;
        local = 0.0;
        children = List.fold_left to_ltacprof_tactic M.empty xs }
-  | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML")
+  | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.")
 
 let feedback_results results =
   Feedback.(feedback
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index dadcfb9f2..f028abde9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -236,7 +236,7 @@ end) = struct
 	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
 	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
-	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
+	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
 	| _, [] ->
 	  (match finalcstr with
 	  | None | Some (_, None) ->
@@ -1424,7 +1424,7 @@ module Strategies =
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
 	  with e when CErrors.noncritical e ->
-            user_err Pp.(str "fold: the term is not unfoldable !")
+            user_err Pp.(str "fold: the term is not unfoldable!")
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad5..efb7e780d 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -24,7 +24,7 @@ let register_alias key tac =
 
 let interp_alias key =
   try KNmap.find key !alias_map
-  with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
+  with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key ++ str ".")
 
 let check_alias key = KNmap.mem key !alias_map
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 10c0319b2..2014f2aff 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -379,7 +379,7 @@ let try_interp_ltac_var coerce ist env (loc,id) =
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
-  with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
+  with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.")
 
 let interp_ident ist env sigma id =
   try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id)