aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-31 12:30:50 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 20:06:05 -0400
commit6a67a0e30bdd96df994dd7d309d1f0d8cc22751f (patch)
tree7f0f8129d69a3dd4fdeacf30dd773bc42e9a95f6 /plugins/funind
parent42d510ceea82d617ac4e630049d690acbe900688 (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 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/glob_termops.ml4
-rw-r--r--plugins/funind/indfun.ml12
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/recdef.ml18
8 files changed, 32 insertions, 32 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0041797de..c2f705898 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -397,7 +397,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
then tclIDTAC g
else
match eq_ids with
- | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
+ | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.");
| eq_id::eq_ids ->
tclTHEN
(tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
@@ -605,7 +605,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
pr_leconstr_env (pf_env g') (project g') new_term_value_eq
);
- anomaly (Pp.str "cannot compute new term value")
+ anomaly (Pp.str "cannot compute new term value.")
in
let fun_body =
mkLambda(Anonymous,
@@ -838,7 +838,7 @@ let build_proof
h_reduce_with_zeta Locusops.onConcl;
build_proof do_finalize new_infos
] g
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -1032,7 +1032,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
ConstRef c -> c
- | _ -> CErrors.anomaly (Pp.str "Not a constant")
+ | _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
}
| _ -> ()
@@ -1255,7 +1255,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
try
let pte =
try destVar (project gl) pte
- with DestKO -> anomaly (Pp.str "Property is not a variable")
+ with DestKO -> anomaly (Pp.str "Property is not a variable.")
in
let fix_info = Id.Map.find pte ptes_to_fix in
let nb_args = fix_info.nb_realargs in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 942527167..a0eb9e2b2 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -44,7 +44,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let id = Namegen.next_ident_away x avoid in
Hashtbl.add tbl id x;
RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
- | Anonymous -> anomaly (Pp.str "Anonymous property binder "))
+ | Anonymous -> anomaly (Pp.str "Anonymous property binder."))
in
let avoid = (Termops.ids_of_context env_with_params ) in
let princ_type_info =
@@ -399,7 +399,7 @@ let get_funs_constant mp dp =
let const = make_con mp dp (Label.of_id id) in
const,i
| Anonymous ->
- anomaly (Pp.str "Anonymous fix")
+ anomaly (Pp.str "Anonymous fix.")
)
na
| _ -> [|const,0|]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 68e097fe9..aa8f918ae 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1115,7 +1115,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
else
CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
- | _ -> anomaly (Pp.str "Should not have an anonymous function here")
+ | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
(* We have renamed all the anonymous functions during alpha_renaming phase *)
end
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0361e8cb1..b99f5a923 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -532,7 +532,7 @@ let rec are_unifiable_aux = function
else
let eqs' =
try (List.combine cpl1 cpl2) @ eqs
- with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
+ with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.")
in
are_unifiable_aux eqs'
@@ -555,7 +555,7 @@ let rec eq_cases_pattern_aux = function
else
let eqs' =
try (List.combine cpl1 cpl2) @ eqs
- with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+ with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.")
in
eq_cases_pattern_aux eqs'
| _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4946285e1..143ce8288 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -734,7 +734,7 @@ let rec add_args id new_args = CAst.map (function
CAppExpl((None,r,None),new_args)
| _ -> b
end
- | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
+ | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
| CProdN(nal,b1) ->
CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
add_args id new_args b1)
@@ -782,9 +782,9 @@ let rec add_args id new_args = CAst.map (function
Miscops.map_cast_type (add_args id new_args) b2)
| CRecord pars ->
CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
- | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
- | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
- | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
+ | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
+ | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
+ | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
)
exception Stop of Constrexpr.constr_expr
@@ -826,7 +826,7 @@ let rec chop_n_arrow n t =
chop_n_arrow new_n t'
with Stop t -> t
end
- | _ -> anomaly (Pp.str "Not enough products")
+ | _ -> anomaly (Pp.str "Not enough products.")
let rec get_args b t : Constrexpr.local_binder_expr list *
@@ -856,7 +856,7 @@ let make_graph (f_ref:global_reference) =
| _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
- | None -> error "Cannot build a graph over an axiom !"
+ | None -> error "Cannot build a graph over an axiom!"
| Some body ->
let env = Global.env () in
let sigma = Evd.from_env env in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2476478ab..a73425543 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -369,7 +369,7 @@ let in_Function : function_info -> Libobject.obj =
let find_or_none id =
try Some
- (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
+ (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
with Not_found -> None
@@ -397,7 +397,7 @@ let add_Function is_general f =
and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
and graph_ind =
match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
- with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
+ with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
in
let finfos =
{ function_constant = f;
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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62eba9513..e6f199dba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -76,7 +76,7 @@ let def_of_const t =
| _ -> raise Not_found)
with Not_found ->
anomaly (str "Cannot find definition of constant " ++
- (Id.print (Label.to_id (con_label (fst sp)))))
+ (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".")
)
|_ -> assert false
@@ -95,7 +95,7 @@ let constant sl s = constr_of_global (find_reference sl s)
let const_of_ref = function
ConstRef kn -> kn
- | _ -> anomaly (Pp.str "ConstRef expected")
+ | _ -> anomaly (Pp.str "ConstRef expected.")
let nf_zeta env =
@@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
travel jinfo new_continuation_tac
{expr_info with info = b; is_final=false} g
end
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
| Prod _ ->
begin
try
@@ -486,7 +486,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos g
| Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
- | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info)
+ | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -1165,7 +1165,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let f_id =
match f_name with
| Name f_id -> next_ident_away_in_goal f_id ids
- | Anonymous -> anomaly (Pp.str "Anonymous function")
+ | Anonymous -> anomaly (Pp.str "Anonymous function.")
in
let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
let n_ids,ids =
@@ -1175,7 +1175,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
| Name id ->
let n_id = next_ident_away_in_goal id ids in
n_id::n_ids,n_id::ids
- | _ -> anomaly (Pp.str "anonymous argument")
+ | _ -> anomaly (Pp.str "anonymous argument.")
)
([],(f_id::ids))
n_names_types
@@ -1302,7 +1302,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| None ->
try add_suffix current_proof_name "_subproof"
with e when CErrors.noncritical e ->
- anomaly (Pp.str "open_new_goal with an unamed theorem")
+ anomaly (Pp.str "open_new_goal with an unamed theorem.")
in
let na = next_global_ident_away name [] in
if Termops.occur_existential sigma gls_type then
@@ -1313,7 +1313,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let na_global = Smartlocate.global_with_alias na_ref in
match na_global with
ConstRef c -> is_opaque_constant c
- | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
+ | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
ref_ := Value (EConstr.Unsafe.to_constr lemma);
@@ -1464,7 +1464,7 @@ let (com_eqn : int -> Id.t ->
let opacity =
match terminate_ref with
| ConstRef c -> is_opaque_constant c
- | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
+ | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
let (evmap, env) = Lemmas.get_current_context() in
let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in