From 961344bd556656b2feb69ce2c0592a5bdcb5c020 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 3 Jun 2016 12:58:58 +0200
Subject: fixing compilation (with Coq trunk & Coq v8.5)

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 2ee0d97..a5037ee 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -2388,7 +2388,7 @@ END
 (* Populating the table *)
 
 let cache_viewhint (_, (i, lvh)) =
-  let mem_raw h = List.exists (Notation_ops.eq_glob_constr h) in
+  let mem_raw h = List.exists (Glob_ops.glob_constr_eq h) in
   let add_hint h hdb = if mem_raw h hdb then hdb else h :: hdb in
   viewtab.(i) <- List.fold_right add_hint lvh viewtab.(i)
 
-- 
cgit v1.2.3