From b994e3195d296e9d12c058127ced381976c3a49e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 31 May 2016 09:09:56 +0200
Subject: Checker: avoid using obsolete names from Names

---
 checker/subtyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/subtyping.ml')

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index e41922573..46d21f6cc 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -103,7 +103,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let eq_projection_body p1 p2 =
     let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check eq_mind (fun x -> x.proj_ind);
+    check MutInd.equal (fun x -> x.proj_ind);
     check (==) (fun x -> x.proj_npars);
     check (==) (fun x -> x.proj_arg);
     check (eq_constr) (fun x -> x.proj_type);
-- 
cgit v1.2.3