From 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 12 Jul 2017 11:44:53 +0200
Subject: Adding a comment regarding De Bruijn universe indices in the kernel.

---
 kernel/mod_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 69fbd0f32..c7f3e5c51 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -98,6 +98,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
           in
+          (** Terms are compared in a context with De Bruijn universe indices *)
 	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
-- 
cgit v1.2.3