From 06b29ed748a9d9b99c2c08a3788906dbad5417d2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Jun 2018 13:57:28 +0200
Subject: Repair relevance marks in-kernel.

Prevent errors when under annotating binders.
---
 kernel/mod_typing.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 421d932d9a..2de5faa6df 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,6 +80,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let c',cst = match cb.const_body with
             | Undef _ | OpaqueDef _ ->
               let j = Typeops.infer env' c in
+              assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
               let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
                   j.uj_type typ in
@@ -101,6 +102,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let cst = match cb.const_body with
             | Undef _ | OpaqueDef _ ->
               let j = Typeops.infer env' c in
+              assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
               let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
                   j.uj_type typ in
-- 
cgit v1.2.3