From 6ec771e10c5af489d8529feea8fdc00beb21a855 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 12:17:05 +0100
Subject: Comment universe operations in Classes.context

---
 vernac/classes.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 748a2628c5..ec01314e46 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -376,9 +376,11 @@ let context poly l =
     | [] -> assert false
     | [_] -> Evd.const_univ_entry ~poly sigma
     | _::_::_ ->
-      (* TODO: explain this little belly dance *)
       if Lib.sections_are_opened ()
       then
+        (* More than 1 variable in a section: we can't associate
+           universes to any specific variable so we declare them
+           separately. *)
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
@@ -386,8 +388,11 @@ let context poly l =
           else Monomorphic_const_entry Univ.ContextSet.empty
         end
       else if poly then
+        (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
         Evd.const_univ_entry ~poly sigma
       else
+        (* Multiple monomorphic axioms: declare universes separately
+           to avoid redeclaring them. *)
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-- 
cgit v1.2.3