Commit bb9003c3 authored by Piotr Trojanek's avatar Piotr Trojanek Committed by Guillaume Melquiond

Minor ocamldoc fixes

parent 88c92346
......@@ -63,10 +63,10 @@ val get_model_trace_label : labels : Slab.t -> Slab.elt
(** {2 Identifiers} *)
type ident = private {
id_string : string; (* non-unique name *)
id_label : Slab.t; (* identifier labels *)
id_loc : Loc.position option; (* optional location *)
id_tag : Weakhtbl.tag; (* unique magical tag *)
id_string : string; (** non-unique name *)
id_label : Slab.t; (** identifier labels *)
id_loc : Loc.position option; (** optional location *)
id_tag : Weakhtbl.tag; (** unique magical tag *)
}
module Mid : Extmap.S with type key = ident
......@@ -78,29 +78,29 @@ val id_compare : ident -> ident -> int
val id_equal : ident -> ident -> bool
val id_hash : ident -> int
(* a user-created type of unregistered identifiers *)
(** a user-created type of unregistered identifiers *)
type preid = {
pre_name : string;
pre_label : Slab.t;
pre_loc : Loc.position option;
}
(* register a pre-ident (you should never use this function) *)
(** register a pre-ident (you should never use this function) *)
val id_register : preid -> ident
(* create a fresh pre-ident *)
(** create a fresh pre-ident *)
val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
(* create a localized pre-ident *)
(** create a localized pre-ident *)
val id_user : ?label:Slab.t -> string -> Loc.position -> preid
(* create a duplicate pre-ident with given labels *)
(** create a duplicate pre-ident with given labels *)
val id_lab : Slab.t -> ident -> preid
(* create a duplicate pre-ident *)
(** create a duplicate pre-ident *)
val id_clone : ?label:Slab.t -> ident -> preid
(* create a derived pre-ident (inherit labels and location) *)
(** create a derived pre-ident (inherit labels and location) *)
val id_derive : ?label:Slab.t -> string -> ident -> preid
(* DEPRECATED : retrieve preid name without registering *)
......
......@@ -53,7 +53,7 @@ val lookup_printer : string -> printer
val list_printers : unit -> (string * Pp.formatted) list
(** {2 use printers} *)
(** {2 Use printers} *)
val print_prelude : prelude pp
val print_th_prelude : task -> prelude_map pp
......@@ -100,7 +100,7 @@ val syntax_arguments_typed :
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** {2 pretty-printing transformations (useful for caching)} *)
(** {2 Pretty-printing transformations (useful for caching)} *)
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
......@@ -114,7 +114,7 @@ val sprint_decl :
('a -> Format.formatter -> Decl.decl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list
(** {2 exceptions to use in transformations and printers} *)
(** {2 Exceptions to use in transformations and printers} *)
exception UnsupportedType of ty * string
exception UnsupportedTerm of term * string
......@@ -127,7 +127,7 @@ val unsupportedPattern : pattern -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented : string -> 'a
(** {3 functions that catch inner error} *)
(** {3 Functions that catch inner error} *)
exception Unsupported of string
(** This exception must be raised only inside a call
......
......@@ -37,12 +37,12 @@ type meta_map = tdecl_set Mmeta.t
type task = task_hd option
and task_hd = private {
task_decl : tdecl; (* last declaration *)
task_prev : task; (* context *)
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_meta : meta_map; (* meta properties *)
task_tag : Weakhtbl.tag; (* unique magical tag *)
task_decl : tdecl; (** last declaration *)
task_prev : task; (** context *)
task_known : known_map; (** known identifiers *)
task_clone : clone_map; (** cloning history *)
task_meta : meta_map; (** meta properties *)
task_tag : Weakhtbl.tag; (** unique magical tag *)
}
val task_equal : task -> task -> bool
......@@ -58,7 +58,7 @@ val task_meta : task -> meta_map
val find_clone_tds : task -> theory -> tdecl_set
val find_meta_tds : task -> meta -> tdecl_set
(** {2 constructors} *)
(** {2 Constructors} *)
val add_decl : task -> decl -> task
val add_tdecl : task -> tdecl -> task
......@@ -67,7 +67,7 @@ val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
val add_meta : task -> meta -> meta_arg list -> task
(** {2 declaration constructors + add_decl} *)
(** {2 Declaration constructors + add_decl} *)
val add_ty_decl : task -> tysymbol -> task
val add_data_decl : task -> data_decl list -> task
......@@ -76,14 +76,14 @@ val add_logic_decl : task -> logic_decl list -> task
val add_ind_decl : task -> ind_sign -> ind_decl list -> task
val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
(** {2 utilities} *)
(** {2 Utilities} *)
val split_theory : theory -> Spr.t option -> task -> task list
(** [split_theory th s t] returns the tasks of [th] added to [t]
that end by one of [s]. They are in the opposite order than
in the theory *)
(** {2 realization utilities} *)
(** {2 Realization utilities} *)
val used_theories : task -> theory Mid.t
(** returns a map from theory names to theories themselves *)
......@@ -97,7 +97,7 @@ val local_decls : task -> theory Mid.t -> decl list
the list of declarations that are not imported
with those theories or derived thereof *)
(** {2 bottom-up, tail-recursive traversal functions} *)
(** {2 Bottom-up, tail-recursive traversal functions} *)
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
......@@ -113,7 +113,7 @@ val task_separate_goal : task -> tdecl * task
goal of the task [t] and [t'] is the rest. raises [GoalNotFound]
if task [t] has no goal *)
(** {2 selectors} *)
(** {2 Selectors} *)
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
......@@ -126,7 +126,7 @@ val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
(* exceptions *)
(** Exceptions *)
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta
......
......@@ -145,7 +145,7 @@ module Mterm : Extmap.S with type key = term
module Sterm : Extset.S with module M = Mterm
module Hterm : Exthtbl.S with type key = term
(** {2 term equality modulo alpha-equivalence and location} *)
(** {2 Term equality modulo alpha-equivalence and location} *)
val t_compare : term -> term -> int
val t_equal : term -> term -> bool
......
......@@ -11,7 +11,7 @@
(** Managing the drivers for external provers *)
(** {2 create a driver} *)
(** {2 Create a driver} *)
type driver
......@@ -22,7 +22,7 @@ val load_driver : Env.env -> string -> string list -> driver
@param string list additional driver files containing only theories
*)
(** {2 use a driver} *)
(** {2 Use a driver} *)
val file_of_task : driver -> string -> string -> Task.task -> string
(** [file_of_task d f th t] produces a filename
......
......@@ -77,7 +77,7 @@ type idpos = {
type 'a goal = private
{ mutable goal_key : 'a;
goal_name : Ident.ident; (** The ident of the task *)
goal_name : Ident.ident; (** ident of the task *)
goal_expl : expl;
goal_parent : 'a goal_parent;
mutable goal_checksum : Termcode.checksum option; (** checksum of the task *)
......@@ -486,7 +486,7 @@ val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
(** {2 Iterators} *)
(** {3 recursive} *)
(** {3 Recursive} *)
val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
(* unused
......@@ -511,7 +511,7 @@ val goal_iter_leaf_goal :
val fold_all_sub_goals_of_theory :
('a -> 'key goal -> 'a) -> 'a -> 'key theory -> 'a
(** {3 not recursive} *)
(** {3 Not recursive} *)
val iter_goal :
('key proof_attempt -> unit) ->
......
......@@ -37,7 +37,7 @@ val fold_product : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
tail-recursive *)
val fold_product_l : ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
(** generalisation of {! Lists.fold_product} not tail-recursive *)
(** generalisation of {! Lists.fold_product}; not tail-recursive *)
val flatten_rev : 'a list list -> 'a list
......
......@@ -39,5 +39,4 @@ val equal : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val compare : ('a -> 'b -> int) -> 'a option -> 'b option -> int
val map_fold :
('a -> 'b -> 'a * 'b) -> 'a -> 'b option -> 'a * 'b option
val map_fold : ('a -> 'b -> 'a * 'b) -> 'a -> 'b option -> 'a * 'b option
......@@ -55,7 +55,7 @@ exception BoolExpected of string * rc_value
type t (** Rc parsed file *)
type section (** section in rc file *)
type section (** Section in rc file *)
type family = (string * section) list (** A family in rc files *)
type simple_family = section list (** A family w/o arguments in rc files*)
......@@ -199,7 +199,7 @@ val from_channel : in_channel -> t
val from_file : string -> t
(** [from_file filename] returns the Rc of the file [filename]
@raise CannotOpen is [filename] does not exist
@raise CannotOpen if [filename] does not exist
@raise SyntaxErrorFile in case of incorrect syntax
@raise ExtraParameters if a section header has more than one argument
*)
......
......@@ -26,28 +26,28 @@ val mapi : (int -> 'a) -> int -> int -> 'a list
val iterf : (float -> unit) -> float -> float -> float -> unit
(** [iterf f min max step] *)
(* Convert fold-like functions into [for_all] and [exists] functions.
Predicates passed to [all], [all2], and [alld] may raise FoldSkip to
signalize [false]. Predicates passed to [any], [any2], and [anyd] may
raise FoldSkip to signalize [true]. *)
(** Convert fold-like functions into [for_all] and [exists] functions.
Predicates passed to [all], [all2], and [alld] may raise FoldSkip to
signalize [false]. Predicates passed to [any], [any2], and [anyd] may
raise FoldSkip to signalize [true]. *)
exception FoldSkip
val all_fn : ('a -> bool) -> 'z -> 'a -> bool
(* [all_fn pr z a] return true if [pr a] is true,
otherwise raises FoldSkip *)
(** [all_fn pr z a] return true if [pr a] is true,
otherwise raise FoldSkip *)
val any_fn : ('a -> bool) -> 'z -> 'a -> bool
(* [all_fn pr z a] return false if [pr a] is false,
otherwise raises FoldSkip *)
(** [any_fn pr z a] return false if [pr a] is false,
otherwise raise FoldSkip *)
val all2_fn : ('a -> 'b -> bool) -> 'z -> 'a -> 'b -> bool
(* [all_fn pr z a b] return true if [pr a b] is true,
otherwise raises FoldSkip *)
(** [all2_fn pr z a b] return true if [pr a b] is true,
otherwise raise FoldSkip *)
val any2_fn : ('a -> 'b -> bool) -> 'z -> 'a -> 'b -> bool
(* [all_fn pr z a b] return false if [pr a b] is false,
otherwise raises FoldSkip *)
(** [any2_fn pr z a b] return false if [pr a b] is false,
otherwise raise FoldSkip *)
type ('z,'a,'c) fold = ('z -> 'a -> 'z) -> 'z -> 'c -> 'z
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
(** Hashtable with weak key used for memoization *)
(** Hashtables with weak key used for memoization *)
type tag
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment