From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 kernel/indTyping.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/indTyping.ml')

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 0d63c8feba..5e294c9729 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -161,7 +161,8 @@ let check_arity env_params env_ar ind =
      full_arity is used as argument or subject to cast, an upper
      universe will be generated *)
   let arity = it_mkProd_or_LetIn arity (Environ.rel_context env_params) in
-  push_rel (LocalAssum (Name ind.mind_entry_typename, arity)) env_ar,
+  let x = Context.make_annot (Name ind.mind_entry_typename) (Sorts.relevance_of_sort ind_sort) in
+  push_rel (LocalAssum (x, arity)) env_ar,
   (arity, indices, univ_info)
 
 let check_constructor_univs env_ar_par univ_info (args,_) =
-- 
cgit v1.2.3