From 6a67a0e30bdd96df994dd7d309d1f0d8cc22751f Mon Sep 17 00:00:00 2001 From: Jason Gross 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 ``` --- pretyping/coercion.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/coercion.ml') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 83c26058a..1282e3cb8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj = if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly (Pp.str "apply_coercion_args") + | _ -> anomaly (Pp.str "apply_coercion_args.") in let res = apply_rec [] funj.uj_type argl in !evdref, res @@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = -- cgit v1.2.3