univ minimization: comment [enforce_uppers]

1 files changed, 5 insertions, 0 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index 764164c52c..e987087242 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