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.

1 files changed, 6 insertions, 4 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0466efa991..3f2a1b075c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -487,11 +487,13 @@ let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  let map (decl, impl) = match impl with
-  | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
-  | _ -> None
+  let map decl =
+    let id = NamedDecl.get_id decl in
+    match Lib.variable_section_kind id with
+    | Implicit -> Some (id, Manual, (true, true))
+    | _ -> None
   in
-  List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx)
+  List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)