diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 6 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
3 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0e4d6e330..a675fe028 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -525,7 +525,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = false; + mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_polymorphic = poly; diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 3015eab25..bd5218eff 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -91,7 +91,11 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in let univs = Univ.UContext.union abs_ctx mib.mind_universes in - { mind_entry_record = mib.mind_record <> None; + let record = match mib.mind_record with + | None -> None + | Some (_, a) -> Some (Array.length a > 0) + in + { mind_entry_record = record; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; mind_entry_inds = inds'; diff --git a/toplevel/record.ml b/toplevel/record.ml index d2aa48db9..896cc41c7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -330,7 +330,7 @@ let declare_structure finite infer poly ctx id idbuild paramimpls params arity f end; let mie = { mind_entry_params = List.map degenerate_decl params; - mind_entry_record = true; + mind_entry_record = Some !primitive_flag; mind_entry_finite = finite != CoFinite; mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; |