diff options
author | 2015-04-23 14:55:11 +0200 | |
---|---|---|
committer | 2015-04-23 16:02:45 +0200 | |
commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
tree | c595fc1fafd00a08cb91e53002610df867cf5eed /plugins/funind/recdef.ml | |
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/funind/recdef.ml')
-rw-r--r-- | plugins/funind/recdef.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |