diff options
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 13 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4771.v | 21 |
2 files changed, 22 insertions, 12 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4626378db6..9173e23b89 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -88,20 +88,9 @@ let subst_reference subst = (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as Print. It is also used for non-evaluable references. *) -open Pp -open Printer let subst_global_reference subst = - let subst_global ref = - let ref',t' = subst_global subst ref in - if not (is_global ref' t') then - (let sigma, env = Pfedit.get_current_context () in - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ - pr_global ref')); - ref' - in - subst_or_var (subst_located subst_global) + subst_or_var (subst_located (subst_global_reference subst)) let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v new file mode 100644 index 0000000000..e25e5a1be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_4771.v @@ -0,0 +1,21 @@ +(* The following code used to trigger an anomaly in functor substitutions *) + +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). |