Fix algebraic comparison with sprop on one side

Close #12909

1 files changed, 6 insertions, 0 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 927db9e9e6..52e93a9e22 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -142,6 +142,12 @@ let enforce_leq_alg u v g =
   | Inl x -> x
   | Inr e -> raise e
 
+let enforce_leq_alg u v g =
+  match Universe.is_sprop u, Universe.is_sprop v with
+  | true, true -> Constraint.empty, g
+  | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None))
+  | false, false -> enforce_leq_alg u v g
+
 (* sanity check wrapper *)
 let enforce_leq_alg u v g =
   let _,g as cg = enforce_leq_alg u v g in