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).

4 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d599afe69..64407f359 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -303,7 +303,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : Context.Rel.t;
+  cs_args : Constr.rel_context;
   cs_concl_realargs : constr array
 }
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index aa53f7e67..8eaef24c4 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int
 val inductive_nparamdecls_env : env -> inductive -> int
 
 (** @return params context *)
-val inductive_paramdecls : pinductive -> Context.Rel.t
-val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
+val inductive_paramdecls : pinductive -> Constr.rel_context
+val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context
 
 (** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> Context.Rel.t
-val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
+val inductive_alldecls : pinductive -> Constr.rel_context
+val inductive_alldecls_env : env -> pinductive -> Constr.rel_context
 
 (** {7 Extract information from a constructor name} *)
 
@@ -141,7 +141,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;    (* internal name of the constructor plus universes *)
   cs_params : constr list;   (* parameters of the constructor in current ctx *)
   cs_nargs : int;            (* length of arguments signature (letin included) *)
-  cs_args : Context.Rel.t;   (* signature of the arguments (letin included) *)
+  cs_args : Constr.rel_context;   (* signature of the arguments (letin included) *)
   cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
 }
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -154,7 +154,7 @@ val get_projections  : env -> inductive_family -> Constant.t array option
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
     part of the inductive family, they appears in the arity *)
-val get_arity        : env -> inductive_family -> Context.Rel.t * Sorts.family
+val get_arity        : env -> inductive_family -> Constr.rel_context * Sorts.family
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d3aa7ac64..efb3c339a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -74,10 +74,10 @@ type typeclass = {
   cl_impl : GlobRef.t;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : GlobRef.t option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Constr.rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : Context.Rel.t;
+  cl_props : Constr.rel_context;
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * hint_info) option
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e4a56960c..80c6d8239 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -35,10 +35,10 @@ type typeclass = {
 
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
       The global reference gives a direct link to the class itself. *)
-  cl_context : GlobRef.t option list * Context.Rel.t;
+  cl_context : GlobRef.t option list * Constr.rel_context;
 
   (** Context of definitions and properties on defs, will not be shared *)
-  cl_props : Context.Rel.t;
+  cl_props : Constr.rel_context;
 
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if