1 files changed, 78 insertions, 10 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index c8e3642be..616a11162 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -10,26 +10,64 @@ open Univ
 open Sign
 (*i*)
 
-(* Unsafe environments. We define here a datatype for environments. 
+(*s Unsafe environments. We define here a datatype for environments. 
    Since typing is not yet defined, it is not possible to check the
    informations added in environments, and that is what we speak here
    of ``unsafe'' environments. *)
 
+type context
 type env
 
+val empty_context : context
 val empty_env : env
 
 val universes : env -> universes
 val context : env -> context
+val rel_context : env -> rel_context
 val var_context : env -> var_context
 
-val push_var : identifier * typed_type -> env -> env
-val change_hyps : 
-  (typed_type signature -> typed_type signature) -> env -> env
-val change_name_rel : env -> int -> identifier -> env
-
-val push_rel : name * typed_type -> env -> env
-
+(* This forgets var and rel contexts *)
+val reset_context : env -> env
+
+(*s This concerns only the context of local vars referred by names
+    [var_context] *)
+val push_var : var_declaration -> env -> env
+val push_var_decl : identifier * typed_type -> env -> env
+val push_var_def : identifier * constr * typed_type -> env -> env
+val change_hyps : (var_context -> var_context) -> env -> env
+val instantiate_vars : var_context -> constr list -> (identifier * constr) list
+val pop_var : identifier -> env -> env
+
+(*s This concerns only the context of local vars referred by indice
+    [rel_context] *)
+val push_rel : rel_declaration -> env -> env
+val push_rel_decl : name * typed_type -> env -> env
+val push_rel_def : name * constr * typed_type -> env -> env
+val push_rels : rel_context -> env -> env
+val names_of_rel_context : env -> names_context
+
+(*s Returns also the substitution to be applied to rel's *)
+val push_rels_to_vars : env -> constr list * env
+
+(* Gives identifiers in var_context and rel_context *)
+val ids_of_context : env -> identifier list
+val map_context : (constr -> constr) -> env -> env
+
+(*s Recurrence on var_context *)
+val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_var_context : (env -> var_declaration -> env) -> env -> env
+
+(* [process_var_context_both_sides f env] iters [f] on the var
+   declarations of env taking as argument both the initial segment, the
+   middle value and the tail segment *)
+val process_var_context_both_sides :
+  (env -> var_declaration -> var_context -> env) -> env -> env 
+
+(*s Recurrence on rel_context *)
+val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_rel_context : (env -> rel_declaration -> env) -> env -> env
+
+(*s add entries to environment *)
 val set_universes : universes -> env -> env
 val add_constraints : constraints -> env -> env
 val add_constant : 
@@ -41,13 +79,34 @@ val add_abstraction :
 
 val new_meta : unit -> int
 
-val lookup_var : identifier -> env -> name * typed_type
-val lookup_rel : int -> env -> name * typed_type
+(*s Looks up in environment *)
+
+(* Looks up in the context of local vars referred by names (var_context) *)
+(* raises [Not_found] if the identifier is not found *)
+val lookup_var_type : identifier -> env -> typed_type
+val lookup_var_value : identifier -> env -> constr option
+val lookup_var : identifier -> env -> constr option * typed_type
+
+(* 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_type : int -> env -> name * typed_type
+val lookup_rel_value : int -> env -> constr option
+
+(* Looks up in the context of global constant names *)
+(* raises [Not_found] if the required path is not found *)
 val lookup_constant : section_path -> env -> constant_body
+
+(* Looks up in the context of global inductive names *)
+(* raises [Not_found] if the required path is not found *)
 val lookup_mind : section_path -> env -> mutual_inductive_body
 
+(*s Miscellanous *)
 val id_of_global : env -> sorts oper -> identifier
 
+val make_all_name_different : env -> env
+
+(*s Functions creating names for anonymous names *)
+
 val id_of_name_using_hdchar : env -> constr -> name -> identifier
 
 (* [named_hd env t na] just returns [na] is it defined, otherwise it
@@ -68,6 +127,15 @@ val prod_name : env -> name * constr * constr -> constr
 val it_lambda_name : env -> constr -> (name * constr) list -> constr
 val it_prod_name : env -> constr -> (name * constr) list -> constr
 
+val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
+
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+
+val it_mkNamedLambda_or_LetIn : constr -> var_context -> constr
+val it_mkNamedProd_or_LetIn : constr -> var_context -> constr
+
 (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
    from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
    name built from [t] *)