diff options
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 |