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

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d1c4a912f2..c9cfd74362 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1070,7 +1070,7 @@ let fake_match_projection env p =
     | NotRecord | FakeRecord -> assert false
     | PrimRecord info ->
       let x, _, _, _ = info.(snd ind) in
-      make_annot (Name x) mip.mind_relevant
+      make_annot (Name x) mip.mind_relevance
   in
   let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in
   let rec fold arg j subst = function
-- 
cgit v1.2.3