Changing the definition of the "Lib.variable.info" type to enable us to do more cleanups

3 files changed, 12 insertions, 22 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index bce7a15cb..3ddef3a9a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -515,14 +515,11 @@ let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  let map (id, impl, _, _) = match impl with
-  | Implicit -> Some (id, Manual, (true, true))
+  let map (decl, impl) = match impl with
+  | Implicit -> Some (Context.Named.Declaration.get_id decl, Manual, (true, true))
   | _ -> None
   in
-  let is_set (_, _, b, _) = match b with
-  | None -> true
-  | Some _ -> false
-  in
+  let is_set = Context.Named.Declaration.is_local_assum % fst in
   List.rev_map map (List.filter is_set ctx)
 
 let adjust_side_condition p = function
diff --git a/library/lib.ml b/library/lib.ml
index 8880a8b15..7fc3e0d9c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -388,7 +388,7 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
 type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
@@ -431,9 +431,8 @@ let extract_hyps (secs,ohyps) =
   let open Context.Named.Declaration in
   let rec aux = function
     | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
-      let (id',b,t) = to_tuple decl in
       let l, r = aux (idl,hyps) in 
-	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
+      (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
     | (Variable (_,_,poly,ctx)::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, if poly then Univ.ContextSet.union r ctx else r
@@ -443,17 +442,12 @@ let extract_hyps (secs,ohyps) =
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
-let instance_from_variable_context sign =
-  let rec inst_rec = function
-    | (id,b,None,_) :: sign -> id :: inst_rec sign
-    | _ :: sign -> inst_rec sign
-    | [] -> [] in
-  Array.of_list (inst_rec sign)
-
-let named_of_variable_context ctx = let open Context.Named.Declaration in
-                                    List.map (function id,_,None,t -> LocalAssum (id,t)
-                                                     | id,_,Some b,t -> LocalDef (id,b,t))
-                                             ctx
+let instance_from_variable_context =
+  let open Context.Named.Declaration in
+  Array.of_list % List.map get_id % List.filter is_local_assum % List.map fst
+
+let named_of_variable_context =
+  List.map fst
   
 let add_section_replacement f g poly hyps =
   match !sectab with
diff --git a/library/lib.mli b/library/lib.mli
index 7080b5dba..092643c2d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -162,8 +162,7 @@ val xml_open_section : (Names.Id.t -> unit) Hook.t
 val xml_close_section : (Names.Id.t -> unit) Hook.t
 
 (** {6 Section management for discharge } *)
-type variable_info = Names.Id.t * Decl_kinds.binding_kind *
-    Term.constr option * Term.types
+type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
 type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t