From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 5 Jun 2018 14:59:15 +0200
Subject: Change the proj_ind field from MutInd.t to inductive.

This is a first step towards the acceptance of mutual record types in the
kernel.
---
 checker/cic.mli      | 2 +-
 checker/subtyping.ml | 2 +-
 checker/typeops.ml   | 2 +-
 checker/values.ml    | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index 3304b032e..ee7914f99 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -207,7 +207,7 @@ type inline = int option
     always transparent. *)
 
 type projection_body = {
-  proj_ind : MutInd.t;
+  proj_ind : inductive;
   proj_npars : int;
   proj_arg : int;
   proj_type : constr; (* Type under params *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index f4ae02084..6a051a5a9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -126,7 +126,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 MutInd.equal (fun x -> x.proj_ind);
+    check eq_ind (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);
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b..345ee5b8f 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(MutInd.equal pb.proj_ind (fst ind));
+    assert(eq_ind pb.proj_ind ind);
     let ty = subst_instance_constr u pb.proj_type in
       substl (c :: List.rev args) ty
 
diff --git a/checker/values.ml b/checker/values.ml
index 31e65729b..c0ddc1908 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
+MD5 2356846eddb0113e5e75bf8b46cddaee checker/cic.mli
 
 *)
 
@@ -225,7 +225,7 @@ let v_cst_def =
 
 let v_projbody =
   v_tuple "projection_body"
-    [|v_cst;Int;Int;v_constr|]
+    [|v_ind;Int;Int;v_constr|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
-- 
cgit v1.2.3