diff options
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4390ff08b..8cbe9c690 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,6 @@ open Stdarg open Tacarg open Misctypes open Globnames -open Term open Genredexpr open Patternops @@ -91,7 +90,7 @@ open Printer 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 + if not (is_global ref' t') then Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; |