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

(limited to 'kernel/environ.ml')

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