diff options
| author | Pierre-Marie Pédrot | 2019-07-31 13:32:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-31 14:35:23 +0200 |
| commit | fc60feb7a3ccd9ec88f6c46929f5fa8172bd7885 (patch) | |
| tree | 309674e4e3debf44ca7c10b07e429f75022c9dd6 /pretyping | |
| parent | 162eefb562aca2c3741ec24d201deb881663e05a (diff) | |
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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/arguments_renaming.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |