From 6d54c0fbbe8c905991dcb99112cce69792c9b142 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 16 Feb 2019 16:47:58 -0800
Subject: Deprecated duplicated explicitation_eq

---
 vernac/comDefinition.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5e74114a86..5eb19eef54 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -35,7 +35,7 @@ let check_imps ~impsty ~impsbody =
     try
       List.for_all (fun (key, (va:bool*bool*bool)) ->
           (* Pervasives.(=) is OK for this type *)
-          Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va)
+          Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va)
         impsbody
     with Not_found -> false
   in
-- 
cgit v1.2.3