Drop '.' from CErrors.anomaly, insert it in args

As per https://github.com/coq/coq/pull/716#issuecomment-305140839

Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```

5 files changed, 8 insertions, 8 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 580c21d40..d66298344 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -582,7 +582,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 2d2dcd0c0..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
 
@@ -55,7 +55,7 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) =
       if overwrite then
         tac_tab := MLTacMap.remove s !tac_tab
       else
-        CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s)
+        CErrors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 594c4fa15..2c09a8b69 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)