diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 10:42:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:19:03 +0100 |
| commit | c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c (patch) | |
| tree | 995ef76564fb951d0dd84a5834d05bbe27b5d239 /interp | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Using a dedicated type for Lib.abstr_info.
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 d1b79ffcd..55f825c25 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 5b4b5f67b..75bfca307 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 3105214d5..ed1cd5276 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 |