diff options
-rw-r--r-- | test-suite/bugs/closed/2417.v | 15 | ||||
-rw-r--r-- | test-suite/success/hintdb_in_ltac.v | 14 | ||||
-rw-r--r-- | test-suite/success/hintdb_in_ltac_bis.v | 15 |
3 files changed, 44 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 000000000..b2f00ffc6 --- /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. diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 000000000..f12b4d1f4 --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,14 @@ +Definition x := 0. + +Hint Unfold x : mybase. + +Ltac autounfoldify base := autounfold with base. + +Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base. + +Goal x = 0. + progress autounfoldify mybase. + Undo. + progress autounfoldify_bis mybase. + trivial. +Qed. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v new file mode 100644 index 000000000..f5c25540e --- /dev/null +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -0,0 +1,15 @@ +Parameter Foo : Prop. +Axiom H : Foo. + +Hint Resolve H : mybase. + +Ltac foo base := eauto with base. + +Tactic Notation "bar" ident(base) := + typeclasses eauto with base. + +Goal Foo. + progress foo mybase. + Undo. + progress bar mybase. +Qed.
\ No newline at end of file |