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

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8928b32f1..deca8afde 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -60,13 +60,13 @@ type stratification = {
 }
 
 type named_context_val = private {
-  env_named_ctx : Context.Named.t;
-  env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
+  env_named_ctx : Constr.named_context;
+  env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
 }
 
 type rel_context_val = private {
-  env_rel_ctx : Context.Rel.t;
-  env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
+  env_rel_ctx : Constr.rel_context;
+  env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
 }
 
 type env = private {
@@ -88,8 +88,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val rel_context   : env -> Context.Rel.t
-val named_context : env -> Context.Named.t
+val rel_context   : env -> Constr.rel_context
+val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
 
 val opaque_tables : env -> Opaqueproof.opaquetab
@@ -108,13 +108,13 @@ val empty_context : env -> bool
 (** {5 Context of de Bruijn variables ([rel_context]) } *)
 
 val nb_rel           : env -> int
-val push_rel         : Context.Rel.Declaration.t -> env -> env
-val push_rel_context : Context.Rel.t -> env -> env
+val push_rel         : Constr.rel_declaration -> env -> env
+val push_rel_context : Constr.rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
 (** Looks up in the context of local vars referred by indice ([rel_context]) 
    raises [Not_found] if the index points out of the context *)
-val lookup_rel    : int -> env -> Context.Rel.Declaration.t
+val lookup_rel    : int -> env -> Constr.rel_declaration
 val lookup_rel_val : int -> env -> lazy_val
 val evaluable_rel : int -> env -> bool
 val env_of_rel     : int -> env -> env
@@ -122,12 +122,12 @@ val env_of_rel     : int -> env -> env
 (** {6 Recurrence on [rel_context] } *)
 
 val fold_rel_context :
-  (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
-val named_context_of_val : named_context_val -> Context.Named.t
-val val_of_named_context : Context.Named.t -> named_context_val
+val named_context_of_val : named_context_val -> Constr.named_context
+val val_of_named_context : Constr.named_context -> named_context_val
 val empty_named_context_val : named_context_val
 val ids_of_named_context_val : named_context_val -> Id.Set.t
 
@@ -138,19 +138,19 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t
 val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
-val push_named : Context.Named.Declaration.t -> env -> env
-val push_named_context : Context.Named.t -> env -> env
+val push_named : Constr.named_declaration -> env -> env
+val push_named_context : Constr.named_context -> env -> env
 val push_named_context_val  :
-    Context.Named.Declaration.t -> named_context_val -> named_context_val
+    Constr.named_declaration -> named_context_val -> named_context_val
 
 
 
 (** Looks up in the context of local vars referred by names ([named_context]) 
    raises [Not_found] if the Id.t is not found *)
 
-val lookup_named     : variable -> env -> Context.Named.Declaration.t
+val lookup_named     : variable -> env -> Constr.named_declaration
 val lookup_named_val : variable -> env -> lazy_val
-val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t
+val lookup_named_ctxt : variable -> named_context_val -> Constr.named_declaration
 val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
@@ -158,13 +158,13 @@ val named_body : variable -> env -> constr option
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
 val fold_named_context :
-  (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
 val set_universes : env -> UGraph.t -> env
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-  ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
+  ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
 
 (** This forgets named and rel contexts *)
 val reset_context : env -> env
@@ -280,7 +280,7 @@ val vars_of_global : env -> constr -> Id.Set.t
 val really_needed : env -> Id.Set.t -> Id.Set.t
 
 (** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> Context.Named.t
+val keep_hyps : env -> Id.Set.t -> Constr.named_context
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
@@ -309,10 +309,10 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 val apply_to_hyp : named_context_val -> variable ->
-  (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
+  (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) ->
     named_context_val
 
-val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val