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

6 files changed, 8 insertions, 8 deletions

diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 0e2b0c80e..751e79d89 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -23,7 +23,7 @@ open Printer
 val traverse :
   Label.t -> constr ->
     (Refset_env.t * Refset_env.t Refmap_env.t *
-     (Label.t * Context.Rel.t * types) list Refmap_env.t)
+     (Label.t * Constr.rel_context * types) list Refmap_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of
diff --git a/vernac/classes.mli b/vernac/classes.mli
index bd30b2d60..9c37364cb 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -16,9 +16,9 @@ open Libnames
 
 (** Errors *)
 
-val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a
 
-val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
+val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
 
 (** Instance declaration *)
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f51bfbad5..b1a9c8a5a 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -82,12 +82,12 @@ val interp_fixpoint :
 val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
 (** Very private function, do not use *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 1d3807502..91caddcf1 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
 
 val explain_inductive_error : inductive_error -> Pp.t
 
-val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t
+val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t
 
 val explain_typeclass_error : env -> typeclass_error -> Pp.t
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index fa6a9adf1..1f401b4e1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -40,7 +40,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: Context.Named.t;
+    ev_hyps: Constr.named_context;
     ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
diff --git a/vernac/record.mli b/vernac/record.mli
index b2c039f0b..f46f59c14 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ val declare_projections :
   bool list ->
   UnivNames.universe_binders ->
   Impargs.manual_implicits list ->
-  Context.Rel.t ->
+  Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
 val definition_structure :