refactored modules structure

[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 a5267b04463b8493bcdf28c72989551611feb182..3059fc098276f15f5fa0bd8f6123d389b39feb48 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -25,6 +25,8 @@
 
 exception Value_not_found of string
 
+(** {2 Types} *)
+
 type value =
   | TermValue of CicNotationPt.term
   | StringValue of string
@@ -41,10 +43,14 @@ type value_type =
 
 type declaration = string * value_type
 type binding = string * (value_type * value)
-type env_type = binding list
+type t = binding list
+
+(** {2 Environment lookup} *)
 
-  (** fills a term pattern instantiating variable magics *)
-val instantiate: env:env_type -> CicNotationPt.term -> CicNotationPt.term
+val lookup_value:   t -> string -> value
+val lookup_num:     t -> string -> string
+val lookup_string:  t -> string -> string
+val lookup_term:    t -> string -> CicNotationPt.term
 
 (** {2 Bindings mangling} *)
 
@@ -57,7 +63,3 @@ val list_binding_of_name: declaration -> binding  (* [] binding *)
 val opt_declaration:  declaration -> declaration  (* t -> OptType t *)
 val list_declaration: declaration -> declaration  (* t -> ListType t *)
 
-(** {2 Debugging} *)
-
-val set_pp_term: (CicNotationPt.term -> string) -> unit
-