From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 Dec 2016 18:00:18 +0100
Subject: Document changes

---
 engine/evd.mli | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 89dcd92cee..86887f3dcc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map
 (*********************************************************
    Sort/universe variables *)
 
-(** Rigid or flexible universe variables *)
+(** Rigid or flexible universe variables.
+
+   [UnivRigid] variables are user-provided or come from an explicit
+   [Type] in the source, we do not minimize them or unify them eagerly.
+
+   [UnivFlexible alg] variables are fresh universe variables of
+   polymorphic constants or generated during refinement, sometimes in
+   algebraic position (i.e. not appearing in the term at the moment of
+   creation). They are the candidates for minimization (if alg, to an
+   algebraic universe) and unified eagerly in the first-order
+   unification heurstic.  *)
 
 type rigid = UState.rigid =
   | UnivRigid
-- 
cgit v1.2.3