From 998093e64d1eae5ed20900e826a081fac54a9eb9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 00:13:00 +0100
Subject: univ minimization: comment compare_constraint_type

---
 engine/universes.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/universes.ml')

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