Repair relevance marks in-kernel.

Prevent errors when under annotating binders.

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index b1d177e76d..2dab14e732 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1946,7 +1946,7 @@ let compile_mind mb mind stack =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
-                 ci_cstr_nargs = [|0|]; ci_relevance = ob.mind_relevant;
+                 ci_cstr_nargs = [|0|]; ci_relevance = ob.mind_relevance;
                  ci_cstr_ndecls = [||] (*FIXME*);
                  ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
       let asw = { asw_ind = ind; asw_prefix = ""; asw_ci = ci;