aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/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 /checker/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 'checker/environ.ml')
-rw-r--r--checker/environ.ml12
1 files changed, 6 insertions, 6 deletions
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 =