From 4a602e4d159c68eaa127e636df0d3445bfe998a2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 25 Jun 2004 00:00:12 +0000
Subject: correspondance des records et noms de champs de records entre un
 module et sa signature

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4811716520..0aa5c99489 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -104,6 +104,7 @@ type one_inductive_body = {
  }
 
 type mutual_inductive_body = {
+  mind_record : bool;
   mind_finite : bool;
   mind_ntypes : int;
   mind_hyps : section_context;
@@ -139,7 +140,8 @@ let subst_mind_packet sub mbp =
 }
 
 let subst_mind sub mib = 
-  { mind_finite = mib.mind_finite ;
+  { mind_record = mib.mind_record ; 
+    mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (assert (mib.mind_hyps=[]); []) ;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
-- 
cgit v1.2.3