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 /pretyping | |
| parent | a006765a56f2af1e0726fa1dd502bf6e9b5d8ced (diff) | |
Fix glob_sort_family for SProp
Fixes #12529
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 2 |
1 files changed, 1 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 |