From 28b51dece32ce57ebac4e0003cd04a04b6094bd1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 24 Oct 2018 16:27:56 +0200
Subject: Comment Environ.set_universes

I looked for this information and forgot about it a couple times so
let's put it in writing.
---
 kernel/environ.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 3d653bcfe0..43bfe7c2fb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -156,6 +156,9 @@ val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 val set_universes : env -> UGraph.t -> env
+(** This is used to update universes during a proof for the sake of
+   evar map-unaware functions, eg [Typing] calling
+   [Typeops.check_hyps_inclusion]. *)
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-- 
cgit v1.2.3