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

1 files changed, 3 insertions, 1 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 481171652..0aa5c9948 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 ;