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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/cic.mli')

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 *)
-- 
cgit v1.2.3