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/declare.ml | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
Using a dedicated type for Lib.abstr_info.
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 5 |
1 files changed, 3 insertions, 2 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) |