diff options
| author | Pierre-Marie Pédrot | 2020-05-09 15:52:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | 2e53445be16ef28058599fed3f06424db17f6943 (patch) | |
| tree | 380085a26541ceb5b79d6a48543362e6a0793715 | |
| parent | 3af3409a8ec23deb3e0d32f00a31363a36f6209b (diff) | |
Add test for #11727, which was indirectly fixed by this PR.
| -rw-r--r-- | test-suite/bugs/closed/bug_11727.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11727.v b/test-suite/bugs/closed/bug_11727.v new file mode 100644 index 0000000000..d346f05c10 --- /dev/null +++ b/test-suite/bugs/closed/bug_11727.v @@ -0,0 +1,8 @@ +Tactic Notation "myunfold" reference(x) := unfold x. +Notation idnat := (@id nat). +Goal let n := 0 in idnat n = 0. +Proof. + intro n. + myunfold idnat. + myunfold n. +Abort. |