Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr

4 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index efb205182..576073344 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