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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/declare.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 } |