Repair relevance marks in-kernel.

Prevent errors when under annotating binders.

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index da5217eb33..de9a052096 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -223,7 +223,7 @@ let subst_mind_packet sub mbp =
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
-    mind_relevant = mbp.mind_relevant;
+    mind_relevance = mbp.mind_relevance;
     mind_nb_constant = mbp.mind_nb_constant;
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }