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, 15 insertions, 14 deletions

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