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

18 files changed, 61 insertions, 61 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 8515d51b0..8bd4b5bfe 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -794,7 +794,7 @@ let drop_parameters depth n argstk =
   try try_drop_parameters depth n argstk
   with Not_found ->
   (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-  anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
+  anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.")
 
 (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a9f212393..4deadff0a 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -26,7 +26,7 @@ module NamedDecl = Context.Named.Declaration
 (*s Cooking the constants. *)
 
 let pop_dirpath p = match DirPath.repr p with
-  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath")
+  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
   | _::l -> DirPath.make l
 
 let pop_mind kn =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9986f439a..5727bf2ea 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -342,7 +342,7 @@ let template_polymorphic_pconstant (cst,u) env =
 let lookup_projection cst env =
   match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
-  | None -> anomaly (Pp.str "lookup_projection: constant is not a projection")
+  | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.")
 
 let is_projection cst env =
   match (lookup_constant cst env).const_proj with 
@@ -546,7 +546,7 @@ let register env field entry =
     | KInt31 (grp, Int31Type) ->
         let i31c = match kind_of_term entry with
                      | Ind i31t -> mkConstructUi (i31t, 1)
-		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
+		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
 	in
         register_one (register_one env (KInt31 (grp,Int31Constructor)) i31c) field entry
     | field -> register_one env field entry
@@ -592,7 +592,7 @@ fun rk value field ->
   let int31_op_from_const n op prim =
     match kind_of_term value with
       | Const kn ->  int31_op n op prim kn
-      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
   in
   let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
   let int31_unop_from_const op prim = int31_op_from_const 1 op prim in
@@ -604,20 +604,20 @@ fun rk value field ->
           match field with
           | KInt31 (grp, Int31Type) -> Retroknowledge.find rk (KInt31 (grp,Int31Bits))
           | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "add_int31_decompilation_from_type called with an abnormal field")
+              (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
         in
         let i31bit_type =
           match kind_of_term int31bit with
           | Ind (i31bit_type,_) -> i31bit_type
           |  _ -> anomaly ~label:"Environ.register"
-              (Pp.str "Int31Bits should be an inductive type")
+              (Pp.str "Int31Bits should be an inductive type.")
         in
         let int31_decompilation =
           match kind_of_term value with
           | Ind (i31t,_) ->
               constr_of_int31 i31t i31bit_type
           | _ -> anomaly ~label:"Environ.register"
-              (Pp.str "should be an inductive type")
+              (Pp.str "should be an inductive type.")
         in
         { empty_reactive_info with
           vm_decompile_const = Some int31_decompilation;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2ff419338..1e13239bf 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -214,7 +214,7 @@ let param_ccls paramsctxt =
 *)
 let typecheck_inductive env mie =
   let () = match mie.mind_entry_inds with
-  | [] -> anomaly (Pp.str "empty inductive types declaration")
+  | [] -> anomaly (Pp.str "empty inductive types declaration.")
   | _ -> ()
   in
   (* Check unicity of names *)
@@ -313,7 +313,7 @@ let typecheck_inductive env mie =
 	      anomaly ~label:"check_inductive" 
 		(Pp.str"Incorrect universe " ++
 		   Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
-		 ++ Universe.pr infu)
+		 ++ Universe.pr infu ++ Pp.str ".")
 	in
 	  RegularArity (not is_natural,full_arity,defu)
       in
@@ -333,7 +333,7 @@ let typecheck_inductive env mie =
 		anomaly ~label:"check_inductive" 
 		  (Pp.str"Incorrect universe " ++
 		     Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
-		   ++ Universe.pr clev)
+		   ++ Universe.pr clev ++ Pp.str ".")
 	      else
 		TemplateArity (param_ccls paramsctxt, infu)
 	  | _ (* Not an explicit occurrence of Type *) ->
@@ -389,11 +389,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.")
 
 (* Check the inductive type is called with the expected parameters *)
 (* [n] is the index of the last inductive type in [env] *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4f4b641b4..f3b03252d 100644
--- a/kernel/inductive.ml
+++ b/kernel/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) =
     Context.Rel.fold_outside
       (fun decl (largs,subs,ty) ->
@@ -1023,7 +1023,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
@@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     || not (Int.equal (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 vdefj = judgment_of_fixpoint recdef in
   let raise_err env i err =
@@ -1061,7 +1061,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 *)
@@ -1100,7 +1100,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/kernel/modops.ml b/kernel/modops.ml
index 0f0056ed4..1f8b97ae6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -265,7 +265,7 @@ let add_retroknowledge mp =
       Environ.register env f e
     |_ ->
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
-        (Pp.str "had to import an unsupported kind of term")
+        (Pp.str "had to import an unsupported kind of term.")
   in
   fun lclrk env ->
   (* The order of the declaration matters, for instance (and it's at the
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 5130aa9a4..d3cd6b62a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -201,47 +201,47 @@ let empty_symbols = [||]
 let get_value tbl i =
   match tbl.(i) with
     | SymbValue v -> v
-    | _ -> anomaly (Pp.str "get_value failed")
+    | _ -> anomaly (Pp.str "get_value failed.")
 
 let get_sort tbl i =
   match tbl.(i) with
     | SymbSort s -> s
-    | _ -> anomaly (Pp.str "get_sort failed")
+    | _ -> anomaly (Pp.str "get_sort failed.")
 
 let get_name tbl i =
   match tbl.(i) with
     | SymbName id -> id
-    | _ -> anomaly (Pp.str "get_name failed")
+    | _ -> anomaly (Pp.str "get_name failed.")
 
 let get_const tbl i =
   match tbl.(i) with
     | SymbConst kn -> kn
-    | _ -> anomaly (Pp.str "get_const failed")
+    | _ -> anomaly (Pp.str "get_const failed.")
 
 let get_match tbl i =
   match tbl.(i) with
     | SymbMatch case_info -> case_info
-    | _ -> anomaly (Pp.str "get_match failed")
+    | _ -> anomaly (Pp.str "get_match failed.")
 
 let get_ind tbl i =
   match tbl.(i) with
     | SymbInd ind -> ind
-    | _ -> anomaly (Pp.str "get_ind failed")
+    | _ -> anomaly (Pp.str "get_ind failed.")
 
 let get_meta tbl i =
   match tbl.(i) with
     | SymbMeta m -> m
-    | _ -> anomaly (Pp.str "get_meta failed")
+    | _ -> anomaly (Pp.str "get_meta failed.")
 
 let get_evar tbl i =
   match tbl.(i) with
     | SymbEvar ev -> ev
-    | _ -> anomaly (Pp.str "get_evar failed")
+    | _ -> anomaly (Pp.str "get_evar failed.")
 
 let get_level tbl i =
   match tbl.(i) with
     | SymbLevel u -> u
-    | _ -> anomaly (Pp.str "get_level failed")
+    | _ -> anomaly (Pp.str "get_level failed.")
 
 let push_symbol x =
   try HashtblSymbol.find symb_tbl x
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3593d94c2..fe9f393f6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -144,7 +144,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
         (* TODO change 0 when we can have de Bruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
-  | _ -> anomaly (Pp.str "Compilation failure") 
+  | _ -> anomaly (Pp.str "Compilation failure.") 
 
 let warn_no_native_compiler =
   let open Pp in
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 26d061768..f6c94158f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -15,7 +15,7 @@ open Envars
 used by the native compiler. *)
 
 let get_load_paths =
-  ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list)
+  ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized.") : unit -> string list)
 
 let open_header = ["Nativevalues";
                    "Nativecode";
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 8d5f6388c..7ffb48221 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -200,7 +200,7 @@ let mk_block tag args =
 (* Two instances of dummy_value should not be pointer equal, otherwise
  comparing them as terms would succeed *)
 let dummy_value : unit -> t =
-  fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed")
+  fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.")
 
 let cast_accu v = (Obj.magic v:accumulator)
 
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 502a10113..59e90ca2e 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -54,8 +54,8 @@ let create cu = Direct ([],cu)
 let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
       if not (Int.Map.mem i tab.opaque_val)
-      then CErrors.anomaly (Pp.str "Indirect in a different table")
-      else CErrors.anomaly (Pp.str "Already an indirect opaque")
+      then CErrors.anomaly (Pp.str "Indirect in a different table.")
+      else CErrors.anomaly (Pp.str "Already an indirect opaque.")
   | Direct (d,cu) ->
       (** Uncomment to check dynamically that all terms turned into
           indirections are hashconsed. *)
@@ -67,21 +67,21 @@ let turn_indirect dp o tab = match o with
         if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
         else if DirPath.equal tab.opaque_dir DirPath.initial then dp
         else CErrors.anomaly
-          (Pp.str "Using the same opaque table for multiple dirpaths") in
+          (Pp.str "Using the same opaque table for multiple dirpaths.") in
       let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
       Indirect ([],dp,id), ntab
 
 let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
-  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque")
+  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
 let iter_direct_opaque f = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
       Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ba714ada2..427ce04c5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -324,7 +324,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	(match kind_of_term a1, kind_of_term a2 with
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
-		 anomaly (Pp.str "conversion was given ill-typed terms (Sort)");
+		 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
 	       sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
@@ -421,7 +421,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         (* Inconsistency: we tolerate that v1, v2 contain shift and update but
            we throw them away *)
         if not (is_empty_stack v1 && is_empty_stack v2) then
-	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda)");
+	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
         let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -429,7 +429,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
-	  anomaly (Pp.str "conversion was given ill-typed terms (FProd)");
+	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
         let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
         ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
@@ -439,7 +439,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let () = match v1 with
         | [] -> ()
         | _ ->
-          anomaly (Pp.str "conversion was given unreduced term (FLambda)")
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
 	eqappr CONV l2r infos
@@ -448,7 +448,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let () = match v2 with
         | [] -> ()
         | _ ->
-	  anomaly (Pp.str "conversion was given unreduced term (FLambda)")
+	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
 	eqappr CONV l2r infos
@@ -767,7 +767,7 @@ let betazeta_appvect = lambda_appvect_assum
 let hnf_prod_app env t n =
   match kind_of_term (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/kernel/term.ml b/kernel/term.ml
index a4296a530..07a85329e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -456,7 +456,7 @@ let lambda_applist c l =
     match kind_of_term c, l with
     | Lambda(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
-    | _ -> anomaly (Pp.str "Not enough lambda's") in
+    | _ -> anomaly (Pp.str "Not enough lambda's.") in
   app [] c l
 
 let lambda_appvect c v = lambda_applist c (Array.to_list v)
@@ -465,11 +465,11 @@ let lambda_applist_assum n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
-      else anomaly (Pp.str "Not enough arguments")
+      else anomaly (Pp.str "Not enough arguments.")
     else match kind_of_term t, l with
     | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
-    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   app n [] c l
 
 let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
@@ -480,7 +480,7 @@ let prod_applist c l =
     match kind_of_term c, l with
     | Prod(_,_,c), arg::l -> app (arg::subst) c l
     | _, [] -> substl subst c
-    | _ -> anomaly (Pp.str "Not enough prod's") in
+    | _ -> anomaly (Pp.str "Not enough prod's.") in
   app [] c l
 
 (* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
@@ -490,11 +490,11 @@ let prod_applist_assum n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
-      else anomaly (Pp.str "Not enough arguments")
+      else anomaly (Pp.str "Not enough arguments.")
     else match kind_of_term t, l with
     | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
-    | _ -> anomaly (Pp.str "Not enough prod/let's") in
+    | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
 let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v)
@@ -660,7 +660,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/kernel/typeops.ml b/kernel/typeops.ml
index dbc0dcb73..1a07bb2fc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -430,10 +430,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_is_type env constr =
   let t = execute env constr in
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 6971c0a2b..487257a77 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -132,7 +132,7 @@ let rec repr g u =
   let a =
     try UMap.find u g.entries
     with Not_found -> CErrors.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 g v
diff --git a/kernel/univ.ml b/kernel/univ.ml
index afe9cbe8d..d53dd8e73 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -781,7 +781,7 @@ let enforce_eq_level u v c =
 let enforce_eq u v c =
   match Universe.level u, Universe.level v with
     | Some u, Some v -> enforce_eq_level u v c
-    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables")
+    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables.")
 
 let check_univ_eq u v = Universe.equal u v
 
@@ -801,13 +801,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, None))
-	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
 
@@ -982,7 +982,7 @@ let enforce_eq_instances x y =
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with")
-		 (Pp.str " instances of different lengths"));
+		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
 type universe_instance = Instance.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f1c0a4f08..629de80f7 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -175,7 +175,7 @@ let subst_of_rel_context_instance sign l =
     | LocalDef (_,c,_)::sign', args' ->
 	aux (substl subst c :: subst) sign' args'
     | [], [] -> subst
-    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match")
+    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
   in aux [] (List.rev sign) l
 
 let adjust_subst_to_rel_context sign l =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 53483a222..21c1225cc 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -236,7 +236,7 @@ let uni_lvl_val (v : values) : Univ.universe_level =
       in
       CErrors.anomaly
         Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
-            ++ pr)
+            ++ pr ++ str ".")
 
 let rec whd_accu a stk =
   let stk =
@@ -285,7 +285,7 @@ let rec whd_accu a stk =
       end
   | tg ->
     CErrors.anomaly
-      Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg)
+      Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".")
 
 external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
 
@@ -308,7 +308,7 @@ let whd_val : values -> whd =
 	   | 1 -> Vfix(Obj.obj o, None)
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
-	   | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
+	   | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
 	else
            Vconstr_block(Obj.obj o)