diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 36d83bb28..acddd2e61 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -228,7 +228,7 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) = let mie = { mind_entry_finite = true; mind_entry_inds = [mie_ind] } in - let sp = declare_mutual_with_eliminations mie in + let sp = declare_mutual_with_eliminations true mie in let rsp = (sp,0) in (* This is ind path of idstruc *) let sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) |