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

1 files changed, 18 insertions, 18 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 4d340399d..181d714ed 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -25,14 +25,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
-val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
+val mkProd_or_LetIn : Constr.rel_declaration -> types -> types
+val mkProd_wo_LetIn : Constr.rel_declaration -> types -> types
+val mkNamedProd_or_LetIn : Constr.named_declaration -> types -> types
+val mkNamedProd_wo_LetIn : Constr.named_declaration -> types -> types
 
 (** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
-val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
+val mkLambda_or_LetIn : Constr.rel_declaration -> constr -> constr
+val mkNamedLambda_or_LetIn : Constr.named_declaration -> constr -> constr
 
 (** {5 Other term constructors. } *)
 
@@ -74,8 +74,8 @@ val to_lambda : int -> constr -> constr
    where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
 val to_prod : int -> constr -> constr
 
-val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : constr -> Constr.rel_context -> constr
+val it_mkProd_or_LetIn : types -> Constr.rel_context -> types
 
 (** In [lambda_applist c args], [c] is supposed to have the form
     [λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -126,29 +126,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> Context.Rel.t * types
+val decompose_prod_assum : types -> Constr.rel_context * types
 
 (** Idem with lambda's and let's *)
-val decompose_lam_assum : constr -> Context.Rel.t * constr
+val decompose_lam_assum : constr -> Constr.rel_context * constr
 
 (** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
+val decompose_prod_n_assum : int -> types -> Constr.rel_context * types
 
 (** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
+val decompose_lam_n_assum : int -> constr -> Constr.rel_context * constr
 
 (** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
+val decompose_lam_n_decls : int -> constr -> Constr.rel_context * constr
 
 (** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> Context.Rel.t
-val lam_assum : constr -> Context.Rel.t
+val prod_assum : types -> Constr.rel_context
+val lam_assum : constr -> Constr.rel_context
 
 (** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> Context.Rel.t
+val prod_n_assum : int -> types -> Constr.rel_context
 
 (** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> Context.Rel.t
+val lam_n_assum : int -> constr -> Constr.rel_context
 
 (** Remove the premisses/parameters of a type/term *)
 val strip_prod : types -> types
@@ -167,7 +167,7 @@ val strip_lam_assum : constr -> constr
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
 
-type arity = Context.Rel.t * Sorts.t
+type arity = Constr.rel_context * Sorts.t
 
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types