aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorppedrot2012-05-30 16:05:13 +0000
committerppedrot2012-05-30 16:05:13 +0000
commit24879dc0e59856e297b0172d00d67df67fbb0184 (patch)
treed57ffef43297aa7f8b29830f3bde7f3bd334babb /interp
parentf9d97c62b2e46829a6ece74d07f5fab2cea1d769 (diff)
More uniformisation in Pp.warn functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r--interp/topconstr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 824b7f59af..1036baf7c1 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -138,7 +138,7 @@ let fold_constr_expr_with_binders g f n acc = function
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (loc,_,_) ->
- Pp.warning "Capture check in multiple binders not done"; acc
+ msg_warning (str "Capture check in multiple binders not done"); acc
let free_vars_of_constr_expr c =
let rec aux bdvars l = function