diff options
Diffstat (limited to 'test-suite/bugs/closed/2417.v')
-rw-r--r-- | test-suite/bugs/closed/2417.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 00000000..b2f00ffc --- /dev/null +++ b/test-suite/bugs/closed/2417.v @@ -0,0 +1,15 @@ +Parameter x y : nat. +Axiom H : x = y. +Hint Rewrite H : mybase. + +Ltac bar base := autorewrite with base. + +Tactic Notation "foo" ident(base) := autorewrite with base. + +Goal x = 0. + bar mybase. + now_show (y = 0). + Undo 2. + foo mybase. + now_show (y = 0). +Abort. |