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 ++++++
 test-suite/bugs/closed/bug_12909.v | 8 ++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12909.v

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
diff --git a/test-suite/bugs/closed/bug_12909.v b/test-suite/bugs/closed/bug_12909.v
new file mode 100644
index 0000000000..fafb6a418f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12909.v
@@ -0,0 +1,8 @@
+Module Type T.
+Axiom A : Type.
+End T.
+
+Module M.
+  Axiom A : SProp.
+End M.
+Fail Module N <: T := M.
-- 
cgit v1.2.3