Module Target

module Target: sig .. end
Datatype and Function for Targets

type non_ident_target =
| Target_hol
| Target_ocaml
| Target_isa
| Target_coq
| Target_tex
| Target_html
| Target_lem
A datatype for Targets. In contrast to the one in this one does not carry white-space information.

type target =
| Target_no_ident of non_ident_target
| Target_ident
target for the typechecked ast is either a real target as in the AST or the identity target
val ast_target_to_target : -> non_ident_target
ast_target_to_target t converts an ast-target to a target. This essentially means dropping the white-space information.
val target_to_ast_target : non_ident_target ->
target_to_ast_target t converts a target t to an ast_target. This essentially means adding empty white-space information.
val ast_target_compare : -> -> int
ast_target_compare is a comparison function for ast-targets.
val target_compare : non_ident_target -> non_ident_target -> int
target_compare is a comparison function for targets.
module Targetmap: sig .. end
target keyed finite maps
module Targetset: Set.S  with type elt = non_ident_target
target sets
val all_targets_list : non_ident_target list
A list of all the targets.
val all_targets : Targetset.t
The set of all the targets.
val all_targets_non_explicit : Targetset.t
The set of targets used when negating or no mentioning explicit targets. Targets like Lem are excluded by default.
val non_ident_target_to_string : non_ident_target -> string
non_ident_target_to_string t returns a string description of a target t.
val target_to_string : target -> string
target_to_string t_opt returns a string description of a target. If some target is given, it does the same as target_to_string. Otherwise, it returns a string description of the identity backend.
val non_ident_target_to_mname : non_ident_target -> Name.t
non_ident_target_to_mname t returns a name for a target. It is similar to non_ident_target_to_string t. However, it returns capitalised versions.
val target_to_output : -> Output.t
target_to_output t returns output for a target t.
val is_human_target : target -> bool
is_human_target targ checks whether targ is a target intended to be read by humans and therefore needs preserving the original structure very closely. Examples for such targets are the tex-, html- and identity-targets.
val dest_human_target : target -> non_ident_target option
dest_human_target targ destructs targ to get the non-identity target. If it s a human-target, None is returned, otherwise the non-identity target.