X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.mli;fp=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.mli;h=7729caef91f92a2b620420fca27238f481c0839b;hb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;hp=877a16f52e6d84bc114b228aad3d3cf6cf009da6;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli
index 877a16f52..7729caef9 100644
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -50,6 +50,8 @@ val value_of_term: CicNotationPt.term -> value
 val term_of_value: value -> CicNotationPt.term
 val well_typed: value_type -> value -> bool
 
+val declarations_of_env: t -> declaration list
+
 (** {2 Environment lookup} *)
 
 val lookup_value:   t -> string -> value
@@ -57,6 +59,8 @@ val lookup_num:     t -> string -> string
 val lookup_string:  t -> string -> string
 val lookup_term:    t -> string -> CicNotationPt.term
 
+val remove:         t -> string -> t
+
 (** {2 Bindings mangling} *)
 
 val opt_binding_some: binding -> binding          (* v -> Some v *)
@@ -68,3 +72,8 @@ val list_binding_of_name: declaration -> binding  (* [] binding *)
 val opt_declaration:  declaration -> declaration  (* t -> OptType t *)
 val list_declaration: declaration -> declaration  (* t -> ListType t *)
 
+(** given a list of environments bindings a set of names n_1, ..., n_k, returns
+ * a single environment where n_i is bound to the list of values bound in the
+ * starting environments *)
+val coalesce_env: declaration list -> t list -> t
+