aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-04 00:13:00 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-13 14:10:04 +0200
commit998093e64d1eae5ed20900e826a081fac54a9eb9 (patch)
treef7ead10ed39bdd979d3dbbd1850c78dc45277b88
parentbc0246f5a570f70c7befb150d7b544032acbaf7e (diff)
univ minimization: comment compare_constraint_type
-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