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.
---
 engine/proofview.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index a725444e81..2d693e0259 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -876,9 +876,9 @@ module Progress = struct
     let eq_named_declaration d1 d2 =
       match d1, d2 with
       | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
-         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
+         Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
       | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
-         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
+         Context.eq_annot Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
          && eq_constr sigma1 sigma2 t1 t2
       | _ ->
          false
-- 
cgit v1.2.3