diff options
| author | Gaëtan Gilbert | 2020-06-17 10:55:35 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-17 10:55:35 +0200 |
| commit | 3083eacd150be7be22192c6a0fc09951891f7e19 (patch) | |
| tree | 4d4ef8a5995be35ba052075ffef683869896851f | |
| parent | a006765a56f2af1e0726fa1dd502bf6e9b5d8ced (diff) | |
Fix glob_sort_family for SProp
Fixes #12529
| -rw-r--r-- | pretyping/glob_ops.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12529.v | 21 |
2 files changed, 22 insertions, 1 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index cb868e0480..342175a512 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -55,7 +55,7 @@ exception ComplexSort let glob_sort_family = let open Sorts in function | UAnonymous {rigid=true} -> InType - | UNamed [GSProp,0] -> InProp + | UNamed [GSProp,0] -> InSProp | UNamed [GProp,0] -> InProp | UNamed [GSet,0] -> InSet | _ -> raise ComplexSort 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). |