diff options
| author | Maxime Dénès | 2017-06-14 17:57:28 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 17:57:28 +0200 |
| commit | d7dc4d4082d76e480b6d9932dcfad64249565e80 (patch) | |
| tree | 47c24efb25606259c3e0d9c2ac4da2160880a47e /test-suite/bugs | |
| parent | 510879170dae6edb989c76a96ded0ed00f192173 (diff) | |
| parent | f713e6c195d1de177b43cab7c2902f5160f6af9f (diff) | |
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/5414.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5414.v b/test-suite/bugs/closed/5414.v new file mode 100644 index 0000000000..2522a274fb --- /dev/null +++ b/test-suite/bugs/closed/5414.v @@ -0,0 +1,12 @@ +(* Use of idents bound to ltac names in a "match" *) + +Definition foo : Type. +Proof. + let x := fresh "a" in + refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)). + exact (a = a). +Defined. +Goal foo. +intros k. elim k. (* elim because elim keeps names *) +intros. +Check a. (* We check that the name is "a" *) |