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.

7 files changed, 25 insertions, 23 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,[])
diff --git a/library/lib.ml b/library/lib.ml
index fa383ab23c..6b01eb07e9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -413,11 +413,8 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-
-type variable_context = variable_info list
 type abstr_info = {
-  abstr_ctx : variable_context;
+  abstr_ctx : Constr.named_context;
   abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
@@ -426,7 +423,6 @@ type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 type secentry =
   | Variable of {
       id:Names.Id.t;
-      kind:Decl_kinds.binding_kind;
     }
   | Context of Univ.ContextSet.t
 
@@ -445,6 +441,9 @@ let empty_section_data ~poly = {
 let sectab =
   Summary.ref ([] : section_data list) ~name:"section-context"
 
+let sec_implicits =
+  Summary.ref Id.Map.empty ~name:"section-implicits"
+
 let check_same_poly p sec =
   if p != sec.sec_poly then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
@@ -458,8 +457,9 @@ let add_section_variable ~name ~kind ~poly =
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | s :: sl ->
        List.iter (fun tab -> check_same_poly poly tab) !sectab;
-       let s = { s with sec_entry = Variable {id=name;kind} :: s.sec_entry } in
-       sectab := s :: sl
+       let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
+       sectab := s :: sl;
+       sec_implicits := Id.Map.add name kind !sec_implicits
 
 let add_section_context ctx =
   match !sectab with
@@ -486,9 +486,9 @@ let is_polymorphic_univ u =
 
 let extract_hyps poly (secs,ohyps) =
   let rec aux = function
-    | (Variable {id;kind}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,kind) :: l, r
+      decl :: l, r
     | (Variable _::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, r
@@ -500,7 +500,7 @@ let extract_hyps poly (secs,ohyps) =
   in aux (secs,ohyps)
 
 let instance_from_variable_context =
-  List.rev_map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+  List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
 
 let extract_worklist info =
   let args = instance_from_variable_context info.abstr_ctx in
@@ -576,6 +576,8 @@ let section_segment_of_reference = let open GlobRef in function
 let variable_section_segment_of_reference gr =
   (section_segment_of_reference gr).abstr_ctx
 
+let variable_section_kind id = Id.Map.get id !sec_implicits
+
 let section_instance = let open GlobRef in function
   | VarRef id ->
      let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index bfee1b16c5..7dc8b52282 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,10 +163,8 @@ val drop_objects : frozen -> frozen
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-type variable_context = variable_info list 
 type abstr_info = private {
-  abstr_ctx : variable_context;
+  abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
   abstr_subst : Univ.Instance.t;
   (** Actual names of the abstracted variables *)
@@ -178,7 +176,8 @@ val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
 val section_segment_of_reference : GlobRef.t -> abstr_info
 
-val variable_section_segment_of_reference : GlobRef.t -> variable_context
+val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
+val variable_section_kind : Id.t -> Decl_kinds.binding_kind
 
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
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)
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 }
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index efe452d5f1..075d89d0df 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -179,7 +179,7 @@ let discharge_class (_,cl) =
   let open CVars in
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
-    ( fun (decl,_) (ctx', subst) ->
+    ( fun decl (ctx', subst) ->
         let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
         (decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in