Swapping Context and Constr: defining declarations on constr in Constr.

This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.

Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).

3 files changed, 8 insertions, 7 deletions

diff --git a/library/global.mli b/library/global.mli
index 57e173cb9..b2a191cee 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,7 +23,7 @@ val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.Named.t
+val named_context : unit -> Constr.named_context
 
 (** {6 Enriching the global environment } *)
 
@@ -79,7 +79,7 @@ val add_module_parameter :
 
 (** {6 Queries in the global environment } *)
 
-val lookup_named     : variable -> Context.Named.Declaration.t
+val lookup_named     : variable -> Constr.named_declaration
 val lookup_constant  : Constant.t -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
diff --git a/library/lib.ml b/library/lib.ml
index 128b27e75..a20de55bf 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -405,7 +405,7 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
 type abstr_info = {
diff --git a/library/lib.mli b/library/lib.mli
index 1d77212e9..5abfccfc7 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Names
+
 (** Lib: record of operations, backtrack, low-level sections *)
 
 (** This module provides a general mechanism to keep a trace of all operations
@@ -153,7 +154,7 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 type variable_context = variable_info list 
 type abstr_info = private {
   abstr_ctx : variable_context;
@@ -165,7 +166,7 @@ type abstr_info = private {
 }
 
 val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Context.Named.t
+val named_of_variable_context : variable_context -> Constr.named_context
 
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
@@ -179,9 +180,9 @@ val is_in_section : GlobRef.t -> bool
 val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Constant.t -> Context.Named.t -> unit
+  Constant.t -> Constr.named_context -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  MutInd.t -> Context.Named.t -> unit
+  MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)