diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 9de0edea81..1823e3a89a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -104,8 +104,9 @@ let process_inductive (sechyps,abs_ctx) modlist mib = let abs_ctx = Univ.instantiate_univ_context abs_ctx in let univs = Univ.UContext.union abs_ctx univs in let record = match mib.mind_record with + | Some (Some (id, _, _)) -> Some (Some id) + | Some None -> Some None | None -> None - | Some (_, a) -> Some (Array.length a > 0) in { mind_entry_record = record; mind_entry_finite = mib.mind_finite; |