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/indtypes.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d14010dbe7..1f357eb292 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -481,7 +481,7 @@ let allowed_sorts env issmall isunit = function
         then logical_sorts else impredicative_sorts
       else logical_sorts
 
-let build_inductive env env_ar finite inds recargs cst =
+let build_inductive env env_ar record finite inds recargs cst =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
@@ -527,7 +527,8 @@ let build_inductive env env_ar finite inds recargs cst =
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)
-  { mind_ntypes = ntypes;
+  { mind_record = record;
+    mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
     mind_packets = packets;
@@ -544,5 +545,6 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let recargs = check_positivity env_arities inds in
   (* Build the inductive packets *)
-  build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+  build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite 
+    inds recargs cst
 
-- 
cgit v1.2.3