snapshot (added typed environment in 2 -> 1 conversion)

[helm.git] / helm / ocaml / cic_notation / cicNotationEnv.mli

diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli
index 3059fc098276f15f5fa0bd8f6123d389b39feb48..877a16f52e6d84bc114b228aad3d3cf6cf009da6 100644 (file)
--- 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