From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 plugins/extraction/extract_env.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction/extract_env.ml')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b59e3b608c..0fa9be21c9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -150,7 +150,7 @@ let check_fix env sg cb i =
     | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible
 
 let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
-  Array.equal Name.equal na1 na2 &&
+  Array.equal (Context.eq_annot Name.equal) na1 na2 &&
   Array.equal (EConstr.eq_constr sg) ca1 ca2 &&
   Array.equal (EConstr.eq_constr sg) ta1 ta2
 
-- 
cgit v1.2.3