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/declarations.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 567850645e..14cfba187e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -91,6 +91,7 @@ type constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
     const_body : Constr.t Mod_subst.substituted constant_def;
     const_type : types;
+    const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : universes;
     const_private_poly_univs : Univ.ContextSet.t option;
@@ -133,7 +134,7 @@ v}
 type record_info =
 | NotRecord
 | FakeRecord
-| PrimRecord of (Id.t * Label.t array * types array) array
+| PrimRecord of (Id.t * Label.t array * Sorts.relevance array * types array) array
 
 type regular_inductive_arity = {
   mind_user_arity : types;
@@ -176,6 +177,8 @@ type one_inductive_body = {
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
+    mind_relevant : Sorts.relevance;
+
 (** {8 Datas for bytecode compilation } *)
 
     mind_nb_constant : int; (** number of constant constructor *)
-- 
cgit v1.2.3


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/declarations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 14cfba187e..5551742c02 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -177,7 +177,7 @@ type one_inductive_body = {
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
-    mind_relevant : Sorts.relevance;
+    mind_relevance : Sorts.relevance;
 
 (** {8 Datas for bytecode compilation } *)
 
-- 
cgit v1.2.3