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/environ.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'checker/environ.ml')

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