diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12529.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12529.v b/test-suite/bugs/closed/bug_12529.v new file mode 100644 index 0000000000..bc3c9a28bd --- /dev/null +++ b/test-suite/bugs/closed/bug_12529.v @@ -0,0 +1,21 @@ +Goal SProp. +match goal with |- SProp => idtac end. +Fail match goal with |- Prop => idtac end. +Abort. + +Goal Prop. +Fail match goal with |- SProp => idtac end. +match goal with |- Prop => idtac end. +Abort. + +Class F A := f : A. + +Inductive pFalse : Prop := . +Inductive sFalse : SProp := . + +Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances. +Definition pf := f : Prop. + +Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances. +Definition sf := (f : SProp). +Definition pf' := (f : Prop). |