Api doc

src/core/task.ml

@@ -227,6 +227,7 @@ let find_tagged_ts t tds acc =
   Stdecl.fold (fun td acc -> match td.td_node with
     | Meta (s, MAts ts :: _) when meta_equal s t -> Sts.add ts acc
     | _ -> assert false) tds.tds_set acc
+(* TODO an exception instead of an assert false (wrong META used) *)
 
 let find_tagged_ls t tds acc =
   begin match t.meta_type with

src/core/theory.mli

@@ -73,6 +73,8 @@ val meta_hash : meta -> int
 
 val register_meta      : string -> meta_arg_type list -> meta
 val register_meta_excl : string -> meta_arg_type list -> meta
+(** Register exclusive meta, each new setting remove the previous one.
+Useful for transformation or printer parameters *)
 
 val lookup_meta : string -> meta
 val list_metas  : unit -> meta list

src/core/ty.mli

@@ -78,11 +78,16 @@ val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
 val ty_var : tvsymbol -> ty
 val ty_app : tysymbol -> ty list -> ty
 
+(** {3 generic traversal functions} *)
+(** traverse only one level of constructor, if you want full traversal
+    you need to call those function inside your function *)
 val ty_map : (ty -> ty) -> ty -> ty
 val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
 val ty_all : (ty -> bool) -> ty -> bool
 val ty_any : (ty -> bool) -> ty -> bool
 
+(** {3 symbol-wise map/fold} *)
+(** visites every symbol of the type} *)
 val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
 val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
 val ty_s_all : (tysymbol -> bool) -> ty -> bool