diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index da223b541..ebf70569d 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -207,9 +207,17 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = array_map_to_list (fun mip -> (mip.mind_typename, - expmod_type oldenv modlist mip.mind_arity, + make_typed_lazy + (expmod_constr oldenv modlist (mind_user_arity mip)) + (fun _ -> level_of_type mip.mind_nf_arity), Array.to_list mip.mind_consnames, - array_map_to_list (expmod_type oldenv modlist) mip.mind_lc)) + Array.to_list + (array_map2 + (fun us nfc -> + make_typed_lazy + (expmod_constr oldenv modlist us) + (fun _ -> level_of_type nfc)) + (mind_user_lc mip) mip.mind_nf_lc))) mib.mind_packets in let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in |