diff options
| author | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
| commit | 47f47713e551f8de18cf2d847f47c1f55b016c8b (patch) | |
| tree | fba8437d2bab7f202181c83a935ff24e865dcc69 /interp | |
| parent | c34744837dae427ac6cb12f5ada198862d8e1e4f (diff) | |
| parent | 4131f060ac42f121685817fcc9546c3899c09ab7 (diff) | |
Merge PR #6425: Cleanup universes in the kernel
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 5 | ||||
| -rw-r--r-- | interp/discharge.ml | 4 | ||||
| -rw-r--r-- | interp/impargs.ml | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index d1b79ffcdd..55f825c251 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -104,7 +104,7 @@ let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in - let hyps,subst,uctx = section_segment_of_constant con in + let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in @@ -333,7 +333,8 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in + let info = section_segment_of_mutual_inductive mind in + let sechyps = info.Lib.abstr_ctx in Some (discharged_hyps kn sechyps, Discharge.process_inductive info repl mie) diff --git a/interp/discharge.ml b/interp/discharge.ml index 5b4b5f67b8..75bfca3078 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -78,8 +78,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Type ar.template_level), true -let process_inductive (section_decls,_,_ as info) modlist mib = - let section_decls = Lib.named_of_variable_context section_decls in +let process_inductive info modlist mib = + let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with diff --git a/interp/impargs.ml b/interp/impargs.ml index 3105214d5e..ed1cd5276c 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -548,7 +548,7 @@ let discharge_implicits (_,(req,l)) = | ImplConstant (con,flags) -> (try let con' = pop_con con in - let vars,_,_ = section_segment_of_constant con in + let vars = variable_section_segment_of_reference (ConstRef con) in let extra_impls = impls_of_context vars in let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in let l' = [ConstRef con',newimpls] in |