+val declaration_of_var: CicNotationPt.pattern_variable -> declaration
+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
+val declarations_of_term: CicNotationPt.term -> declaration list
+val combine: declaration list -> value list -> t (** @raise Invalid_argument *)
+