From edd11666d9e23f917929b57485010d4288d8beb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 26 Aug 2020 16:13:49 +0200
Subject: Fix algebraic comparison with sprop on one side

Close #12909
---
 kernel/uGraph.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/uGraph.ml')

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