diff options
| author | Emilio Jesus Gallego Arias | 2019-11-26 19:00:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-26 19:00:09 +0100 |
| commit | 8ca4bcd16b87b2c5de0050f0b3f0765ef9130342 (patch) | |
| tree | 398f2515b2070758da2c536f98c144cc32abbed5 | |
| parent | d7879b8566e48aabfdbee5c27bd4c29691352233 (diff) | |
| parent | 11337dac57824fc96c91cba7c4d0bc6d1c068068 (diff) | |
Merge PR #11166: Add test for #11161
Reviewed-by: ejgallego
| -rw-r--r-- | test-suite/bugs/closed/bug_11161.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v new file mode 100644 index 0000000000..22a075e096 --- /dev/null +++ b/test-suite/bugs/closed/bug_11161.v @@ -0,0 +1,10 @@ +(* Ensure that evars are properly normalized in the instance path. + Problems with this can cause eg #11161. *) + +Class Foo (n:nat) := {x : bool}. + +Instance bar n : Foo n. Admitted. + +Instance bar' n : Foo n. split. abstract exact true. Qed. + +Instance bar'' n : Foo n. split. abstract exact true. Defined. |