diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 14:55:11 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 16:02:45 +0200 |
| commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
| tree | c595fc1fafd00a08cb91e53002610df867cf5eed /plugins | |
| parent | 915c8f15965fe8e7ee9d02a663fd890ef80539ad (diff) | |
Remove almost all the uses of string concatenation when building error messages.
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
3 files changed, 13 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 45e5aaf54..a2bbf97ae 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -604,7 +604,8 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f) + errorlabstrm "FunInd.build_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in @@ -636,10 +637,12 @@ let build_case_scheme fa = (* let id_to_constr id = *) (* Constrintern.global_reference id *) (* in *) - let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) - with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + let funs = + let (_,f,_) = fa in + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + with Not_found -> + errorlabstrm "FunInd.build_case_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 738ade8ca..1c409500e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,9 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Constrintern.locate_reference princ_ref - with Not_found -> Errors.error ("cannot find "^ Id.to_string id) + with Not_found -> + Errors.errorlabstrm "IndFun.const_of_id" + (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = match (Term.kind_of_term t) with diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0999b95d7..b9902a9fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,7 +305,8 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then error ("check_not_nested : failure "^Id.to_string x) + then errorlabstrm "Recdef.check_not_nested" + (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b |