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 ``` --- plugins/rtauto/proof_search.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/rtauto') diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 4eef1b0a7..153a6a49a 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -145,7 +145,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.") type 'a with_deps = {dep_it:'a; @@ -167,7 +167,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.") let pop n prf = let nprf= @@ -361,7 +361,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -386,7 +386,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.") with Not_found -> search_norev seq @@ -464,7 +464,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly (Pp.str "already succeeded") + | Complete prf -> anomaly (Pp.str "already succeeded.") open Pp -- cgit v1.2.3