diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-31 12:30:50 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-02 20:06:05 -0400 |
commit | 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch) | |
tree | 7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /kernel/environ.ml | |
parent | 42d510ceea82d617ac4e630049d690acbe900688 (diff) |
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
```
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r-- | kernel/environ.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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; |