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/indtypes.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3173dc5383..009eb3da38 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive env specif in
   let env' =
-    let r = (snd (fst specif)).mind_relevant in
+    let r = (snd (fst specif)).mind_relevance in
     let anon = Context.make_annot Anonymous r in
     let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
     push_rel decl env in
@@ -486,7 +486,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d)
         splayed_lc in
-    let mind_relevant = match arity with
+    let mind_relevance = match arity with
       | RegularArity { mind_sort;_ } -> Sorts.relevance_of_sort mind_sort
       | TemplateArity _ -> Sorts.Relevant
     in
@@ -517,7 +517,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 	mind_user_lc = lc;
 	mind_nf_lc = nf_lc;
         mind_recargs = recarg;
-        mind_relevant;
+        mind_relevance;
         mind_nb_constant = !nconst;
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
-- 
cgit v1.2.3