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/funind/invfun.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 12232dd83..f373e486c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -140,7 +140,7 @@ let generate_type evd g_to_f f graph i = let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with - | [] | [_] -> anomaly (Pp.str "Not a valid context") + | [] | [_] -> anomaly (Pp.str "Not a valid context.") | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function @@ -292,7 +292,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun (_,pat) acc -> match pat with | IntroNaming (IntroIdentifier id) -> id::acc - | _ -> anomaly (Pp.str "Not an identifier") + | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) [] @@ -401,7 +401,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes Array.map (fun ((_,(ctxt,concl))) -> match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") | hres::res::decl::ctxt -> let res = EConstr.it_mkLambda_or_LetIn (EConstr.it_mkProd_or_LetIn concl [hres;res]) @@ -708,7 +708,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = then let eq_lemma = try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") in tclTHENSEQ[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; @@ -938,7 +938,7 @@ let revert_graph kn post_tac hid g = let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly (Pp.str "Cannot retrieve infos about a mutual block") + anomaly (Pp.str "Cannot retrieve infos about a mutual block.") in (* if we can find a completeness lemma for this function then we can come back to the functional form. If not, we do nothing -- cgit v1.2.3