From fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Jul 2019 13:32:25 +0200
Subject: Specialize the section API.

We split the function used to retrieve the local context from the one used to
provide the implicit status of each binder. Most of the users only rely on the
former indeed.
---
 tactics/declare.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 63e9279edc..61f9c3b1c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -71,8 +71,7 @@ let load_constant i ((sp,kn), obj) =
 
 let cooking_info segment =
   let modlist = replacement_context () in
-  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
-  let named_ctx = List.map fst hyps in
+  let { abstr_ctx = named_ctx; abstr_subst = subst; abstr_uctx = uctx } = segment in
   let abstract = (named_ctx, subst, uctx) in
   { Opaqueproof.modlist; abstract }
 
-- 
cgit v1.2.3