From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/2417.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/bugs/closed/2417.v (limited to 'test-suite/bugs/closed/2417.v') 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. -- cgit v1.2.3