aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--engine/universes.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/universes.ml b/engine/universes.ml
index 1b1ce7cec..ca6ce7184 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -705,6 +705,7 @@ let pr_universe_body = function
let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
+(* Eq < Le < Lt *)
let compare_constraint_type d d' =
match d, d' with
| Eq, Eq -> 0