ocaml 3.09 transition

[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 7729caef91f92a2b620420fca27238f481c0839b..d4f87097e2fa2c50d86a56b6b55d985e2a72032c 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationEnv.mli
+++ b/helm/ocaml/cic_notation/cicNotationEnv.mli
@@ -23,8 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Value_not_found of string
-
 (** {2 Types} *)
 
 type value =
@@ -41,6 +39,13 @@ type value_type =
   | OptType of value_type
   | ListType of value_type
 
+  (** looked up value not found in environment *)
+exception Value_not_found of string
+
+  (** looked up value has the wrong type
+   * parameters are value name and value type in environment *)
+exception Type_mismatch of string * value_type
+
 type declaration = string * value_type
 type binding = string * (value_type * value)
 type t = binding list
@@ -51,15 +56,23 @@ 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 *)
 
 (** {2 Environment lookup} *)
 
-val lookup_value:   t -> string -> value
-val lookup_num:     t -> string -> string
-val lookup_string:  t -> string -> string
+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:         t -> string -> t
+val remove_name:    t -> string -> t
+val remove_names:   t -> string list -> t
 
 (** {2 Bindings mangling} *)