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 ``` --- checker/reduction.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'checker/reduction.ml') diff --git a/checker/reduction.ml b/checker/reduction.ml index 82f09cf4b..ba0b01784 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr univ CONV infos (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) | (_, FLambda _) -> if v2 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr univ CONV infos (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) @@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true let hnf_prod_app env t n = match whd_all env t with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl -- cgit v1.2.3