From 3083eacd150be7be22192c6a0fc09951891f7e19 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 17 Jun 2020 10:55:35 +0200
Subject: Fix glob_sort_family for SProp

Fixes #12529
---
 pretyping/glob_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3