From c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 10:42:41 +0100
Subject: Using a dedicated type for Lib.abstr_info.

---
 interp/declare.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp/declare.ml')

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)
 
-- 
cgit v1.2.3