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

8 files changed, 25 insertions, 30 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 0798d385d..3e3523d76 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -686,7 +686,8 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
     let n =
       try
         let vars = Lib.variable_section_segment_of_reference r in
-        List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+        let open Context.Named.Declaration in
+        vars |> List.map fst |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,Lib.discharge_global r,n,l,[])
diff --git a/kernel/names.ml b/kernel/names.ml
index 9267a64d6..d673c91e8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -82,6 +82,9 @@ struct
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  let mk_name id =
+    Name id
+
   let is_anonymous = function
     | Anonymous -> true
     | Name _ -> false
diff --git a/kernel/names.mli b/kernel/names.mli
index feaedc775..0af1cde8f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -82,6 +82,9 @@ sig
   type t = Anonymous     (** anonymous identifier *)
 	 | Name of Id.t  (** non-anonymous identifier *)
 
+  val mk_name : Id.t -> t
+  (** constructor *)
+
   val is_anonymous : t -> bool
   (** Return [true] iff a given name is [Anonymous]. *)
 
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
 
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fb..bf9063fdb 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -48,7 +48,7 @@ let discharge_rename_args = function
      (try 
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
-       let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+       let var_names = List.map (Name.mk_name % Context.Named.Declaration.get_id % fst) vars in
        let names' = List.map (fun l -> var_names @ l) names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9ea..9fff64ae5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -197,12 +197,10 @@ let subst_class (subst,cl) =
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
-    ( fun (n,_,b,t) (ctx', subst) ->
-        let decl = match b with
-                   | None -> LocalAssum (Name n, substn_vars 1 subst t)
-		   | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
-	in
-	(decl :: ctx', n :: subst)
+    ( fun (decl,_) (ctx', subst) ->
+        let open Context.Named.Declaration in
+        let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in
+	(decl' :: ctx', Context.Named.Declaration.get_id decl :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in