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 /checker/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 'checker/environ.ml')
-rw-r--r-- | checker/environ.ml | 12 |
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 = |