diff options
Diffstat (limited to 'ltac/tacsubst.ml')
| -rw-r--r-- | ltac/tacsubst.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 1326818fc..3f504b7f3 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -93,7 +93,7 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (eq_constr (Universes.constr_of_global ref') t') then - msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ + Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' |