diff options
| -rw-r--r-- | library/declare.ml | 18 | ||||
| -rw-r--r-- | vernac/command.ml | 5 | ||||
| -rw-r--r-- | vernac/discharge.ml | 28 |
3 files changed, 29 insertions, 22 deletions
diff --git a/library/declare.ml b/library/declare.ml index f3150174c..fcaadaa6e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -356,6 +356,21 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_private = None; }) +(* reinfer subtyping constraints for inductive after section is dischared. *) +let infer_inductive_subtyping (pth, mind_ent) = + if mind_ent.mind_entry_polymorphic then + begin + let env = Global.env () in + let env' = + Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env + in + let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in + let evd = Evd.from_env env'' in + (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent) + end + else (pth, mind_ent) + + type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = @@ -365,7 +380,8 @@ let inInductive : inductive_obj -> obj = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive } + discharge_function = discharge_inductive; + rebuild_function = infer_inductive_subtyping } let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in diff --git a/vernac/command.ml b/vernac/command.ml index 35b75370e..2d4f05134 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -660,7 +660,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_private = if prv then Some false else None; mind_entry_universes = ground_uinfind; } - in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls + in + (if poly then + Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent + else mind_ent), pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 21ffa4cbf..c7a741c13 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -111,24 +111,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib = | Some None -> Some None | None -> None in - let mind_ent = - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_polymorphic = mib.mind_polymorphic; - mind_entry_private = mib.mind_private; - mind_entry_universes = univ_info_ind - } - in - if mib.mind_polymorphic then - begin - let env = Global.env () in - let env' = Environ.push_context univs env in - let (env'', typed_params) = Typeops.infer_local_decls env' params' in - let evd = Evd.from_env env'' in - Inductiveops.infer_inductive_subtyping env'' evd mind_ent - end - else - mind_ent + { mind_entry_record = record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds'; + mind_entry_polymorphic = mib.mind_polymorphic; + mind_entry_private = mib.mind_private; + mind_entry_universes = univ_info_ind + } |