- (** fills a term pattern instantiating variable magics *)
-val instantiate: env:env_type -> CicNotationPt.term -> CicNotationPt.term
+(** {2 Environment lookup} *)
+
+val lookup_value: t -> string -> value (** @raise Value_not_found *)
+
+(** lookup_* functions below may raise Value_not_found and Type_mismatch *)
+
+val lookup_term: t -> string -> CicNotationPt.term
+val lookup_string: t -> string -> string
+val lookup_num: t -> string -> string
+val lookup_opt: t -> string -> value option
+val lookup_list: t -> string -> value list
+
+val remove_name: t -> string -> t
+val remove_names: t -> string list -> t