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=877a16f52e6d84bc114b228aad3d3cf6cf009da6;hb=ea6b99ed26a954a578e3c88909479dcf9cab7345;hp=3059fc098276f15f5fa0bd8f6123d389b39feb48;hpb=dbcc29c0e46454c7e31b485135900ceab38627e1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli
index 3059fc098..877a16f52 100644
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -45,6 +45,11 @@ type declaration = string * value_type
 type binding = string * (value_type * value)
 type t = binding list
 
+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
+
 (** {2 Environment lookup} *)
 
 val lookup_value:   t -> string -> value