CLEANUP: Type alias "Context.section_context" was removed

8 files changed, 8 insertions, 12 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 4c88283ca..94fcfb486 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -428,5 +428,3 @@ module NamedList =
 
     let fold f l ~init = List.fold_right f l init
   end
-
-type section_context = Named.t
diff --git a/kernel/context.mli b/kernel/context.mli
index 8ed09794b..c5da51381 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -263,5 +263,3 @@ sig
 
   val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 end
-
-type section_context = Named.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index db09e5ed7..f5059cd75 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -154,7 +154,7 @@ type inline = bool
 type result =
   constant_def * constant_type * projection_body option * 
     bool * constant_universes * inline
-    * Context.section_context option
+    * Context.Named.t option
 
 let on_body ml hy f = function
   | Undef _ as x -> x
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 327e697d2..eb4073096 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -19,7 +19,7 @@ type inline = bool
 type result =
   constant_def * constant_type * projection_body option * 
     bool * constant_universes * inline
-    * Context.section_context option
+    * Context.Named.t option
 
 val cook_constant : env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f89773fcc..fe2fa6d7f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -78,7 +78,7 @@ type typing_flags = {
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
 type constant_body = {
-    const_hyps : Context.section_context; (** New: younger hyp at top *)
+    const_hyps : Context.Named.t; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted option;
@@ -177,7 +177,7 @@ type mutual_inductive_body = {
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Context.Named.t;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index df2c4653f..b736b2113 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
-  const_entry_secctx : Context.section_context option;
+  const_entry_secctx : Context.Named.t option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
@@ -73,7 +73,7 @@ type 'a definition_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Context.section_context option * bool * types Univ.in_universe_context * inline 
+    Context.Named.t option * bool * types Univ.in_universe_context * inline 
 
 type projection_entry = {
   proj_entry_ind : mutual_inductive;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b5e576435..77451d8ea 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -232,7 +232,7 @@ val vars_of_global : env -> constr -> Id.Set.t
 val really_needed : env -> Id.Set.t -> Id.Set.t
 
 (** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> Context.section_context
+val keep_hyps : env -> Id.Set.t -> Context.Named.t
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 2112284ea..81fd1427d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -127,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
   constant_type
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> Context.section_context -> unit
+val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit