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

13 files changed, 35 insertions, 34 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 955ff4c08..0cb8c7afc 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s =
     | [] ->
 	anomaly ~label:locstr (str "cannot find " ++ str s ++
 	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-	prlist_with_sep pr_comma pr_dirpath dirs)
+	prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
     | l ->
       anomaly ~label:locstr
 	(str "ambiguous name " ++ str s ++ str " can represent " ++
 	   prlist_with_sep pr_comma
 	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
 	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
-	   prlist_with_sep pr_comma pr_dirpath dirs)
+	   prlist_with_sep pr_comma pr_dirpath dirs ++ str ".")
 
 (* For tactics/commands requiring vernacular libraries *)
 
@@ -185,7 +185,7 @@ let build_bool_type () =
     andb_prop =  init_reference ["Datatypes"] "andb_prop";
     andb_true_intro =  init_reference ["Datatypes"] "andb_true_intro" }
 
-let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.")
 
 let build_sigma_type () =
   { proj1 = init_reference ["Specif"] "projT1";
@@ -368,7 +368,7 @@ let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
 let coq_jmeq_ref     = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
 let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
-let coq_existS_ref  = lazy (anomaly (Pp.str "use coq_existT_ref"))
+let coq_existS_ref  = lazy (anomaly (Pp.str "use coq_existT_ref."))
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_exist_ref  = lazy (init_reference ["Specif"] "exist")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
diff --git a/library/declare.ml b/library/declare.ml
index 29aa08e77..7d0edbc8b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
       obj.cst_was_seff <- false;  
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
-      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".")
     end else
       let () = check_exists sp in
       let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -385,7 +385,7 @@ let declare_projections mind =
 let declare_mind mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
-    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
+    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
   let isrecord,isprim = declare_projections mind in
@@ -400,7 +400,7 @@ let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
   Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> anomaly (Pp.str "no recursive definition")
+  | [] -> anomaly (Pp.str "no recursive definition.")
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
 	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
@@ -415,7 +415,7 @@ let fixpoint_message indexes l =
 
 let cofixpoint_message l =
   Flags.if_verbose Feedback.msg_info (match l with
-  | [] -> anomaly (Pp.str "No corecursive definition")
+  | [] -> anomaly (Pp.str "No corecursive definition.")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
                     spc () ++ str "are corecursively defined"))
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 08c33b5c1..c98d4a7f3 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -252,7 +252,7 @@ let in_modkeep : Lib.lib_objects -> obj =
 
 let do_modtype i sp mp sobjs =
   if Nametab.exists_modtype sp then
-    anomaly (pr_path sp ++ str " already exists");
+    anomaly (pr_path sp ++ str " already exists.");
   Nametab.push_modtype (Nametab.Until i) sp mp;
   ModSubstObjs.set mp sobjs
 
@@ -883,7 +883,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
       (* If not, let's do it now ... *)
       let mp' = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
-        anomaly (Pp.str "Unexpected disk module name");
+        anomaly (Pp.str "Unexpected disk module name.");
   in
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
diff --git a/library/global.ml b/library/global.ml
index 5fa710b36..1ba86699d 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -44,7 +44,7 @@ let () =
 let assert_not_parsing () =
   if !Flags.we_are_parsing then
     CErrors.anomaly (
-      Pp.strbrk"The global environment cannot be accessed during parsing")
+      Pp.strbrk"The global environment cannot be accessed during parsing.")
 
 let safe_env () = assert_not_parsing(); !global_env
 
diff --git a/library/globnames.ml b/library/globnames.ml
index a78f5f13a..9aeb37973 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -242,4 +242,4 @@ let pop_global_reference = function
   | ConstRef con -> ConstRef (pop_con con)
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
-  | VarRef id -> anomaly (Pp.str "VarRef not poppable")
+  | VarRef id -> anomaly (Pp.str "VarRef not poppable.")
diff --git a/library/goptions.ml b/library/goptions.ml
index a803771cb..a305214e8 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -273,23 +273,23 @@ type 'a write_function = 'a -> unit
 let declare_int_option =
   declare_option
     (fun v -> IntValue v)
-    (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
-    (fun _ _ -> anomaly (Pp.str "async_option"))
+    (function IntValue v -> v | _ -> anomaly (Pp.str "async_option."))
+    (fun _ _ -> anomaly (Pp.str "async_option."))
 let declare_bool_option =
   declare_option
     (fun v -> BoolValue v)
-    (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
-    (fun _ _ -> anomaly (Pp.str "async_option"))
+    (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option."))
+    (fun _ _ -> anomaly (Pp.str "async_option."))
 let declare_string_option =
   declare_option
     (fun v -> StringValue v)
-    (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (function StringValue v -> v | _ -> anomaly (Pp.str "async_option."))
     (fun x y -> x^","^y)
 let declare_stringopt_option =
   declare_option
     (fun v -> StringOptValue v)
-    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
-    (fun _ _ -> anomaly (Pp.str "async_option"))
+    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
+    (fun _ _ -> anomaly (Pp.str "async_option."))
 
 (* 3- User accessible commands *)
 
diff --git a/library/heads.ml b/library/heads.ml
index 02465f22f..3adfe0fd2 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -72,7 +72,8 @@ let kind_of_head env t =
        with Not_found ->
          CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
-               str (Names.Constant.to_string cst)))
+               str (Names.Constant.to_string cst) ++
+               str "."))
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/impargs.ml b/library/impargs.ml
index 885185da1..8f3bfc17e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -291,16 +291,16 @@ let is_status_implicit = function
   | _ -> true
 
 let name_of_implicit = function
-  | None -> anomaly (Pp.str "Not an implicit argument")
+  | None -> anomaly (Pp.str "Not an implicit argument.")
   | Some (id,_,_) -> id
 
 let maximal_insertion_of = function
   | Some (_,_,(b,_)) -> b
-  | None -> anomaly (Pp.str "Not an implicit argument")
+  | None -> anomaly (Pp.str "Not an implicit argument.")
 
 let force_inference_of = function
   | Some (_, _, (_, b)) -> b
-  | None -> anomaly (Pp.str "Not an implicit argument")
+  | None -> anomaly (Pp.str "Not an implicit argument.")
 
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
@@ -324,7 +324,7 @@ let positions_of_implicits (_,impls) =
 
 let rec prepare_implicits f = function
   | [] -> []
-  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit")
+  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
   | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
       Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
diff --git a/library/kindops.ml b/library/kindops.ml
index 21b1bec33..623d2537a 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
 
 let string_of_definition_kind def =
   let (locality, poly, kind) = def in
-  let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
+  let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in
   match kind with
   | Definition ->
     begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
     | Global -> "Global Instance"
     end
   | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    CErrors.anomaly (Pp.str "Internal definition kind")
+    CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/lib.ml b/library/lib.ml
index 4ad4e261d..9d71a854f 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -350,7 +350,7 @@ let end_compilation_checks dir =
     try match find_entry_p is_opening_lib with
       |	(oname, CompilingLibrary prefix) -> oname
       | _ -> assert false
-    with Not_found -> anomaly (Pp.str "No module declared")
+    with Not_found -> anomaly (Pp.str "No module declared.")
   in
   let _ =
     match !lib_state.comp_name with
@@ -358,7 +358,7 @@ let end_compilation_checks dir =
       | Some m ->
 	  if not (Names.DirPath.equal m dir) then anomaly
 	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
-             spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
+             spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str ".");
   in
   oname
 
@@ -547,7 +547,7 @@ let discharge_item ((sp,_ as oname),e) =
   | FrozenState _ -> None
   | ClosedSection _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
-      anomaly (Pp.str "discharge_item")
+      anomaly (Pp.str "discharge_item.")
 
 let close_section () =
   let oname,fs =
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 529b9502b..ad429ea84 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -29,7 +29,7 @@ let physical p = p.path_physical
 let get_load_paths () = !load_paths
 
 let anomaly_too_many_paths path =
-  anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
+  anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".")
 
 let find_load_path phys_dir =
   let phys_dir = CUnix.canonical_path_name phys_dir in
diff --git a/library/nametab.ml b/library/nametab.ml
index 2e4e98013..93e9c03ce 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -294,7 +294,7 @@ module DirPath' =
 struct
   include DirPath
   let repr dir = match DirPath.repr dir with
-    | [] -> anomaly (Pp.str "Empty dirpath")
+    | [] -> anomaly (Pp.str "Empty dirpath.")
     | id :: l -> (id, l)
 end
 
diff --git a/library/summary.ml b/library/summary.ml
index d9f644100..c7bf95fd4 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -46,7 +46,7 @@ let declare_summary sumname decl =
   let () = if Int.Map.mem hash !summaries then
     let (name, _) = Int.Map.find hash !summaries in
     anomaly ~label:"Summary.declare_summary"
-      (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name)
+      (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
   in
   all_declared_summaries := Int.Set.add hash !all_declared_summaries;
   summary_names := (hash, sumname) :: !summary_names;
@@ -85,10 +85,10 @@ let unfreeze_summaries fs =
    * may modify the content of [summaries] ny loading new ML modules *)
   let (_, decl) =
     try Int.Map.find ml_modules_summary !summaries
-    with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules)
+    with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
   in
   let () = match fs.ml_module with
-  | None -> anomaly (str "Undeclared summary " ++ str ml_modules)
+  | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
   | Some state -> decl.unfreeze_function state
   in
   let fold id (_, decl) states =