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

8 files changed, 32 insertions, 32 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 6d93c11ea..b3b403425 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -165,7 +165,7 @@ let find_logical_path phys_dir =
   match List.filter2 (fun p d -> p = phys_dir) physical logical with
   | _,[dir] -> dir
   | _,[] -> default_root_prefix
-  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
+  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^"."))
 
 let remove_load_path dir =
   let physical, logical = !load_paths in
@@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) =
 	    end
       | _,[] ->
 	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
+      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
 
 let load_paths_of_dir_path dir =
   let physical, logical = !load_paths in
diff --git a/checker/environ.ml b/checker/environ.ml
index bce40861c..22d1eec17 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -106,7 +106,7 @@ let anomaly s = anomaly (Pp.str s)
 
 let add_constant kn cs env =
   if Cmap_env.mem kn env.env_globals.env_constants then
-    Printf.ksprintf anomaly ("Constant %s is already defined")
+    Printf.ksprintf anomaly ("Constant %s is already defined.")
       (Constant.to_string kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
@@ -161,7 +161,7 @@ let is_projection cst env =
 let lookup_projection p env =
   match (lookup_constant (Projection.constant p) env).const_proj with 
   | Some pb -> pb
-  | None -> anomaly ("lookup_projection: constant is not a projection")
+  | None -> anomaly ("lookup_projection: constant is not a projection.")
 
 (* Mutual Inductives *)
 let scrape_mind env kn=
@@ -182,7 +182,7 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    Printf.ksprintf anomaly ("Inductive %s is already defined")
+    Printf.ksprintf anomaly ("Inductive %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
@@ -201,7 +201,7 @@ let add_mind kn mib env =
 
 let add_modtype ln mtb env =
   if MPmap.mem ln env.env_globals.env_modtypes then
-    Printf.ksprintf anomaly ("Module type %s is already defined")
+    Printf.ksprintf anomaly ("Module type %s is already defined.")
       (ModPath.to_string ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
@@ -211,7 +211,7 @@ let add_modtype ln mtb env =
 
 let shallow_add_module mp mb env =
   if MPmap.mem mp env.env_globals.env_modules then
-    Printf.ksprintf anomaly ("Module %s is already defined")
+    Printf.ksprintf anomaly ("Module %s is already defined.")
       (ModPath.to_string mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
@@ -221,7 +221,7 @@ let shallow_add_module mp mb env =
 
 let shallow_remove_module mp env =
   if not (MPmap.mem mp env.env_globals.env_modules) then
-    Printf.ksprintf anomaly ("Module %s is unknown")
+    Printf.ksprintf anomaly ("Module %s is unknown.")
       (ModPath.to_string mp);
   let new_mods = MPmap.remove mp env.env_globals.env_modules in
   let new_globals =
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 0482912b0..c9ee326cb 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t =
         let env1 = push_rel (LocalDef (name,def,ty)) env in
 	sorts_of_constr_args env1 c
     | _ when is_constructor_head t -> []
-    | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
+    | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.")
 
 
 (* Prop and Set are small *)
@@ -302,11 +302,11 @@ let failwith_non_pos n ntypes c =
 
 let failwith_non_pos_vect n ntypes v =
   Array.iter (failwith_non_pos n ntypes) v;
-  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
+  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.")
 
 let failwith_non_pos_list n ntypes l =
   List.iter (failwith_non_pos n ntypes) l;
-  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
+  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
 
 (* Conclusion of constructors: check the inductive type is called with
    the expected parameters *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 9e417a8eb..f890adba9 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c =
 
 let instantiate_params full t u args sign =
   let fail () =
-    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
+    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
   let (rem_args, subs, ty) =
     fold_rel_context
       (fun decl (largs,subs,ty) ->
@@ -986,7 +986,7 @@ let check_one_fix renv recpos trees def =
             List.iter (check_rec_call renv []) l;
             check_rec_call renv [] c
 
-        | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+        | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
 
 	| Sort _ -> assert (l = [])
 
@@ -1004,7 +1004,7 @@ let check_one_fix renv recpos trees def =
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
 	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
-	| _ -> anomaly (Pp.str "Not enough abstractions in fix body")
+	| _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
 	    
   in
   check_rec_call renv [] def
@@ -1018,7 +1018,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     || Array.length names <> nbfix
     || bodynum < 0
     || bodynum >= nbfix
-  then anomaly (Pp.str "Ill-formed fix term");
+  then anomaly (Pp.str "Ill-formed fix term.");
   let fixenv = push_rec_types recdef env in
   let raise_err env i err =
     error_ill_formed_rec_body env err names i in
@@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
 		    raise_err env i (RecursionNotOnInductiveType a) in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
-            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
+            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
@@ -1073,7 +1073,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 exception CoFixGuardError of env * guard_error
 
 let anomaly_ill_typed () =
-  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
+  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.")
 
 let rec codomain_is_coind env c =
   let b = whd_all env c in
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 82f09cf4b..ba0b01784 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
         if v1 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
         eqappr univ CONV infos
           (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
     | (_, FLambda _) ->
         if v2 <> [] then
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).");
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
         eqappr univ CONV infos
           (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true
 let hnf_prod_app env t n =
   match whd_all env t with
     | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
 
 let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
diff --git a/checker/term.ml b/checker/term.ml
index 8cac78375..75c566aeb 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -333,7 +333,7 @@ let destArity =
     | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | Sort s          -> l,s
-    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
   in
   prodec_rec []
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1396d56df..0163db334 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -262,7 +262,7 @@ let rec execute env cstr =
 
     | Rel n -> judge_of_relative env n
 
-    | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+    | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
 
     | Const c -> judge_of_constant env c
 
@@ -344,10 +344,10 @@ let rec execute env cstr =
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly (Pp.str "the kernel does not support metavariables")
+	anomaly (Pp.str "the kernel does not support metavariables.")
 
     | Evar _ ->
-	anomaly (Pp.str "the kernel does not support existential variables")
+	anomaly (Pp.str "the kernel does not support existential variables.")
 
 and execute_type env constr =
   let j = execute env constr in
diff --git a/checker/univ.ml b/checker/univ.ml
index fb1a0faa7..571743231 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -545,7 +545,7 @@ let repr g u =
     let a =
       try UMap.find u g
       with Not_found -> anomaly ~label:"Univ.repr"
-	  (str"Universe " ++ Level.pr u ++ str" undefined")
+	  (str"Universe " ++ Level.pr u ++ str" undefined.")
     in
     match a with
       | Equiv v -> repr_rec v
@@ -848,7 +848,7 @@ let merge g arcu arcv =
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
       match between g arcu arcv with
-      | [] -> anomaly (str "Univ.between")
+      | [] -> anomaly (str "Univ.between.")
       | arc::rest ->
         let (max_rank, old_max_rank, best_arc, rest) =
           List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
@@ -911,7 +911,7 @@ let enforce_univ_eq u v g =
       | FastLT -> error_inconsistency Eq u v
       | FastLE -> merge g arcv arcu
       | FastNLE -> merge_disc g arcu arcv
-      | FastEQ -> anomaly (Pp.str "Univ.compare"))
+      | FastEQ -> anomaly (Pp.str "Univ.compare."))
 
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -924,7 +924,7 @@ let enforce_univ_leq u v g =
     | FastLT -> error_inconsistency Le u v
     | FastLE  -> merge g arcv arcu
     | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
+    | FastEQ -> anomaly (Pp.str "Univ.compare.")
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
@@ -937,7 +937,7 @@ let enforce_univ_lt u v g =
     | FastNLE ->
       match fast_compare_neq false g arcv arcu with
 	FastNLE -> fst (setlt g arcu arcv)
-      | FastEQ -> anomaly (Pp.str "Univ.compare")
+      | FastEQ -> anomaly (Pp.str "Univ.compare.")
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
@@ -995,13 +995,13 @@ let constraint_add_leq v u c =
       else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
 	if Level.equal x y then (* u+(k+1) <= u *)
 	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
       else if j = 0 then
 	Constraint.add (x,Le,y) c
       else (* j >= 1 *) (* m = n + k, u <= v+k *)
 	if Level.equal x y then c (* u <= u+k, trivial *)
 	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
-	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
 	  
 let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
 
@@ -1012,7 +1012,7 @@ let enforce_leq u v c =
   match v with
   | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) ->
     Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
 
 let enforce_leq u v c =
   if check_univ_leq u v then c