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

(limited to 'kernel/declareops.ml')

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 }
-- 
cgit v1.2.3