diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 11:44:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-12 11:44:53 +0200 |
| commit | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (patch) | |
| tree | 5beee0d40d95aa08f3f0030cb419c63894679238 /kernel/mod_typing.ml | |
| parent | 91df402729f70144a4e4d198c4384dc515920e59 (diff) | |
Adding a comment regarding De Bruijn universe indices in the kernel.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 _ -> |