From 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 31 May 2017 12:30:50 -0400
Subject: 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
```
---
 checker/inductive.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'checker/inductive.ml')

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
-- 
cgit v1.2.3