diff options
| author | Maxime Dénès | 2017-08-16 09:41:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-16 09:41:04 +0200 |
| commit | ffd6a20eb807cdd381d511e7b59799495122591d (patch) | |
| tree | 814c9fce26132606f89388b25f163b836cf66af9 /test-suite | |
| parent | 96d53d99d32f7006e553c6772b9c983925fb31f6 (diff) | |
| parent | d01e3b07470ab326f5754332ac812f21794721bc (diff) | |
Merge PR #841: Timorous fix of bug #5598 on global existing class in sections
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5598.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5598.v b/test-suite/bugs/closed/5598.v new file mode 100644 index 0000000000..55fef1a575 --- /dev/null +++ b/test-suite/bugs/closed/5598.v @@ -0,0 +1,8 @@ +(* Checking when discharge of an existing class is possible *) +Section foo. + Context {T} (a : T) (b : T). + Let k := eq_refl a. + Existing Class eq. + Fail Global Existing Instance k. + Existing Instance k. +End foo. |