From 02372d2ce62bec843b34ca65f87f6619871fe931 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sun, 4 Mar 2018 01:20:22 +0100
Subject: univ minimization: comment [enforce_uppers]

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

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index 764164c52..e98708724 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -811,6 +811,11 @@ let not_lower lower (d,l) =
          (** No constraint existing on l *) true) l
 
 exception UpperBoundedAlg
+(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
+   constraints to [lbound], adding them to [cstrs].
+
+    @raise UpperBoundedAlg if any [upper] constraints are strict and
+   [lbound] algebraic. *)
 let enforce_uppers upper lbound cstrs =
   List.fold_left (fun cstrs (d, r) ->
       if d == Univ.Le then
-- 
cgit v1.2.3