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.

---
 pretyping/reductionops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ac88468545..78de0437d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -121,10 +121,10 @@ module ReductionBehaviour = struct
     let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
 
   let discharge = function
-    | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+    | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
       let b =
-        if Lib.is_in_section (ConstRef c) then
-          let vars, _, _ = Lib.section_segment_of_constant c in
+        if Lib.is_in_section gr then
+          let vars = Lib.variable_section_segment_of_reference gr in
           let extra = List.length vars in
           let nargs' =
              if b.b_nargs = max_int then max_int
-- 
cgit v1.2.3