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.
---
 pretyping/arguments_renaming.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 534c0ca20b..a86d237164 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -47,7 +47,7 @@ let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) ->
      (try 
        let vars = Lib.variable_section_segment_of_reference c in
-       let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
+       let var_names = List.map (NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
        Some (ReqGlobal (c, names), (c, names'))
      with Not_found -> Some req)
-- 
cgit v1.2.3