aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-31 12:30:50 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 20:06:05 -0400
commit6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch)
tree7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /kernel/environ.ml
parent42d510ceea82d617ac4e630049d690acbe900688 (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.ml12
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;