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 0e2b0c80e8..751e79d89c 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 bd30b2d60e..9c37364cb0 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 f51bfbad59..b1a9c8a5a3 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 1d38075022..91caddcf13 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 fa6a9adf1b..1f401b4e15 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 b2c039f0b5..f46f59c14d 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 :