diff options
| author | Maxime Dénès | 2020-06-23 12:30:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-06-23 12:30:52 +0200 |
| commit | 5d65a6617333aea66be3c819f3fe53dd30e95f77 (patch) | |
| tree | cde88b78823c4479727562e28684669df65fc564 /pretyping | |
| parent | 700918ada1c864c900bdc065d39c4b16d2a47500 (diff) | |
| parent | 3083eacd150be7be22192c6a0fc09951891f7e19 (diff) | |
Merge PR #12530: Fix glob_sort_family for SProp
Reviewed-by: gares
Reviewed-by: maximedenes
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 |