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
```

9 files changed, 20 insertions, 20 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index bf274901b..726115653 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -131,7 +131,7 @@ let lookup_constant_in_impl cst fallback =
        - The label has not been found in the structure. This is an error *)
     match fallback with
       | Some cb -> cb
-      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
+      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst ++ str ".")
 
 let lookup_constant cst =
   try
@@ -146,7 +146,7 @@ let lookup_mind_in_impl mind =
     let fields = memoize_fields_of_mp mp in
       search_mind_label lab fields
   with Not_found ->
-    anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind)
+    anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".")
 
 let lookup_mind mind =
   try Global.lookup_mind mind
diff --git a/vernac/command.ml b/vernac/command.ml
index 87e7e50ec..0f9dee12c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -674,7 +674,7 @@ let extract_coercions indl =
 let extract_params indl =
   let paramsl = List.map (fun (_,params,_,_) -> params) indl in
   match paramsl with
-  | [] -> anomaly (Pp.str "empty list of inductive types")
+  | [] -> anomaly (Pp.str "empty list of inductive types.")
   | params::paramsl ->
       if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
 	"Parameters should be syntactically the same for each inductive type.");
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index b898f3e83..65ade7887 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -23,7 +23,7 @@ let detype_param =
   function
   | LocalAssum (Name id, p) -> id, LocalAssumEntry p
   | LocalDef (Name id, p,_) -> id, LocalDefEntry p
-  | _ -> anomaly (Pp.str "Unnamed inductive local variable")
+  | _ -> anomaly (Pp.str "Unnamed inductive local variable.")
 
 (* Replace
 
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 040c86805..021fde961 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -109,7 +109,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) =
   let () =
     if not allow_uncaught && not (CErrors.handled (fst e)) then
       let (e, info) = e in
-      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) in
+      let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in
       let err = CErrors.make_anomaly msg in
       Util.iraise (err, info)
   in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 045eed3e1..77e356eb2 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function
     let recguard,ordered_inds = find_mutually_recursive_statements thms in
     let thms = List.map pi2 ordered_inds in
     Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
-  | [] -> anomaly (Pp.str "Empty list of theorems")
+  | [] -> anomaly (Pp.str "Empty list of theorems.")
 
 (* Saving a goal *)
 
@@ -242,7 +242,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
         | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
         | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
         | App (t, args) -> mkApp (body_i t, args)
-        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in
       let body_i = body_i body in
       match locality with
       | Discharge ->
@@ -402,7 +402,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       let () = match thms with [_] -> () | _ -> assert false in
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
-  | [] -> anomaly (Pp.str "No proof to start")
+  | [] -> anomaly (Pp.str "No proof to start.")
   | ((id,pl),(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 42494dd28..34b9b97d8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -250,7 +250,7 @@ let rec find_pattern nt xl = function
   | _, [] ->
       user_err Pp.(str msg_expected_form_of_recursive_notation)
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
-      anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right")
+      anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
 
 let rec interp_list_parser hd = function
   | [] -> [], List.rev hd
@@ -271,7 +271,7 @@ let rec interp_list_parser hd = function
   | NonTerminal _ as x :: tl ->
       let xyl,tl' = interp_list_parser [x] tl in
       xyl, List.rev_append hd tl'
-  | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser")
+  | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
 
 
 (* Find non-terminal tokens of notation *)
@@ -645,7 +645,7 @@ let make_production etyps symbols =
             let tkl = List.flatten
               (List.map (function Terminal s -> [CLexer.terminal s]
                 | Break _ -> []
-                | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in
+                | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in
 	    match List.assoc x etyps with
             | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll
             | ETBinder o ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b0b35aed5..6dee95bc5 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -64,7 +64,7 @@ let subst_evar_constr evs n idf t =
 	      ev_hyps = hyps ; ev_chop = chop } =
 	  try evar_info k
 	  with Not_found ->
-	    anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found")
+	    anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
 	in
         seen := Int.Set.add id !seen;
 	  (* Evar arguments are created in inverse order,
@@ -325,7 +325,7 @@ type program_info = program_info_aux CEphemeron.key
 let get_info x =
   try CEphemeron.get x
   with CEphemeron.InvalidKey ->
-    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
+    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.")
 
 let assumption_message = Declare.assumption_message
 
@@ -1166,7 +1166,7 @@ let next_obligation n tac =
   let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
   let i = match Array.findi is_open obls with
   | Some i -> i
-  | None -> anomaly (Pp.str "Could not find a solvable obligation")
+  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
   in
   solve_obligation prg i tac
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 5accc8e37..f8e12f4ee 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -174,7 +174,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 let degenerate_decl decl =
   let id = match RelDecl.get_name decl with
     | Name id -> id
-    | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
+    | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in
   match decl with
     | LocalAssum (_,t) -> (id, LocalAssumEntry t)
     | LocalDef (_,b,_) -> (id, LocalDefEntry b)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 77be7f454..c6ec89c5e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -67,7 +67,7 @@ let show_node () =
       could, possibly, be cleaned away. (Feb. 2010) *)
   ()
 
-let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO")
+let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -1918,10 +1918,10 @@ let interp ?proof ?loc locality poly c =
   | VernacToplevelControl e -> raise e
 
   (* Resetting *)
-  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm")
-  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm")
-  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm")
-  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm")
+  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
+  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
+  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
+  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
 
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")