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, 16 insertions, 16 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 913825a9f..ecb36615f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -321,7 +321,7 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
-  val to_named_context : (t, types) Context.Named.pt -> Context.Named.t
+  val to_named_context : (t, types) Context.Named.pt -> Constr.named_context
 
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 8ce1b625f..135aa73fc 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -128,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option
     [nf_evar]. *)
 
 val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 type undefined_evars_cache
@@ -161,7 +161,7 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 64db70451..d638bb2d3 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -230,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option
 
 val existential_opt_value0 : evar_map -> existential -> constr option
 
-val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
diff --git a/engine/termops.mli b/engine/termops.mli
index f9aa6ba63..80988989f 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
+val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr
 
 (** {6 Generic iterators on constr} *)
 
@@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context
 (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
    [n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
    starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
-val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
+val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context
 
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
@@ -239,19 +239,19 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 (** other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
-val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
-val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
-val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
+val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context
+val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context
+val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *)
 
 val map_rel_context_in_env :
-  (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
+  (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context
 val map_rel_context_with_binders :
   (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
 val fold_named_context_both_sides :
-  ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
-    Context.Named.t -> init:'a -> 'a
+  ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
+    Constr.named_context -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
-val compact_named_context : Context.Named.t -> Context.Compacted.t
+val compact_named_context : Constr.named_context -> Constr.compacted_context
 
 val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
 val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
@@ -313,6 +313,6 @@ val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
 val print_constr     : constr -> Pp.t
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
 val print_named_context : env -> Pp.t
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t
+val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
 val print_env : env -> Pp.t