From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
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.
---
 kernel/declareops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1b73096f7f..ad5167d8be 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -84,7 +84,7 @@ let subst_const_def sub def = match def with
   | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)
 
 let subst_const_proj sub pb =
-  { pb with proj_ind = subst_mind sub pb.proj_ind;
+  { pb with proj_ind = subst_ind sub pb.proj_ind;
     proj_type = subst_mps sub pb.proj_type;
   }
 
-- 
cgit v1.2.3