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.

2 files changed, 7 insertions, 5 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)
diff --git a/interp/notation.ml b/interp/notation.ml
index d88182241b..a78bc60e83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1533,7 +1533,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
     let n =
       try
         let vars = Lib.variable_section_segment_of_reference r in
-        vars |> List.map fst |> List.filter is_local_assum |> List.length
+        vars |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,r,n,l,[])