package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Refset' : CSig.SetS with type elt = Names.GlobRef.t
module Refmap' : CSig.MapS with type key = Names.GlobRef.t
val safe_basename_of_global : Names.GlobRef.t -> Names.Id.t
val warning_axioms : unit -> unit
val warning_opaques : bool -> unit
val warning_ambiguous_name : ?loc:Loc.t -> (Libnames.qualid * Names.ModPath.t * Names.GlobRef.t) -> unit
val warning_id : string -> unit
val error_axiom_scheme : ?loc:Loc.t -> Names.GlobRef.t -> int -> 'a
val error_constant : ?loc:Loc.t -> Names.GlobRef.t -> 'a
val error_inductive : ?loc:Loc.t -> Names.GlobRef.t -> 'a
val error_nb_cons : unit -> 'a
val error_module_clash : Names.ModPath.t -> Names.ModPath.t -> 'a
val error_no_module_expr : Names.ModPath.t -> 'a
val error_singleton_become_prop : Names.Id.t -> Names.GlobRef.t option -> 'a
val error_unknown_module : ?loc:Loc.t -> Libnames.qualid -> 'a
val error_scheme : unit -> 'a
val error_not_visible : Names.GlobRef.t -> 'a
val error_MPfile_as_mod : Names.ModPath.t -> bool -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
val check_loaded_modfile : Names.ModPath.t -> unit
val msg_of_implicit : Miniml.kill_reason -> string
val err_or_warn_remaining_implicit : Miniml.kill_reason -> unit
val info_file : string -> unit
val occur_kn_in_ref : Names.MutInd.t -> Names.GlobRef.t -> bool
val modpath_of_r : Names.GlobRef.t -> Names.ModPath.t
val label_of_r : Names.GlobRef.t -> Names.Label.t
val is_modfile : Names.ModPath.t -> bool
val string_of_modfile : Names.ModPath.t -> string
val file_of_modfile : Names.ModPath.t -> string
val is_toplevel : Names.ModPath.t -> bool
val at_toplevel : Names.ModPath.t -> bool
val mp_length : Names.ModPath.t -> int
val prefixes_mp : Names.ModPath.t -> Names.MPset.t
val common_prefix_from_list : Names.ModPath.t -> Names.ModPath.t list -> Names.ModPath.t option
val get_nth_label_mp : int -> Names.ModPath.t -> Names.Label.t
val labels_of_ref : Names.GlobRef.t -> Names.ModPath.t * Names.Label.t list
val add_inductive_kind : Names.MutInd.t -> Miniml.inductive_kind -> unit
val is_coinductive : Names.GlobRef.t -> bool
val is_coinductive_type : Miniml.ml_type -> bool
val get_record_fields : Names.GlobRef.t -> Names.GlobRef.t option list
val record_fields_of_type : Miniml.ml_type -> Names.GlobRef.t option list
val add_recursors : Environ.env -> Names.MutInd.t -> unit
val is_recursor : Names.GlobRef.t -> bool
val add_projection : int -> Names.Constant.t -> Names.inductive -> unit
val is_projection : Names.GlobRef.t -> bool
val projection_arity : Names.GlobRef.t -> int
val projection_info : Names.GlobRef.t -> Names.inductive * int
val add_info_axiom : Names.GlobRef.t -> unit
val remove_info_axiom : Names.GlobRef.t -> unit
val add_log_axiom : Names.GlobRef.t -> unit
val add_opaque : Names.GlobRef.t -> unit
val remove_opaque : Names.GlobRef.t -> unit
val reset_tables : unit -> unit
val access_opaque : unit -> bool
val auto_inline : unit -> bool
val type_expand : unit -> bool
val keep_singleton : unit -> bool
type opt_flag = {
  1. opt_kill_dum : bool;
  2. opt_fix_fun : bool;
  3. opt_case_iot : bool;
  4. opt_case_idr : bool;
  5. opt_case_idg : bool;
  6. opt_case_cst : bool;
  7. opt_case_fun : bool;
  8. opt_case_app : bool;
  9. opt_let_app : bool;
  10. opt_lin_let : bool;
  11. opt_lin_beta : bool;
}
val optims : unit -> opt_flag
val conservative_types : unit -> bool
val file_comment : unit -> string
type lang =
  1. | Ocaml
  2. | Haskell
  3. | Scheme
  4. | JSON
val lang : unit -> lang
val set_modular : bool -> unit
val modular : unit -> bool
val set_library : bool -> unit
val library : unit -> bool
val set_extrcompute : bool -> unit
val is_extrcompute : unit -> bool
val to_inline : Names.GlobRef.t -> bool
val to_keep : Names.GlobRef.t -> bool
val implicits_of_global : Names.GlobRef.t -> Int.Set.t
val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
val is_custom : Names.GlobRef.t -> bool
val is_inline_custom : Names.GlobRef.t -> bool
val find_custom : Names.GlobRef.t -> string
val find_type_custom : Names.GlobRef.t -> string list * string
val is_custom_match : Miniml.ml_branch array -> bool
val find_custom_match : Miniml.ml_branch array -> string
val extraction_language : lang -> unit
val extraction_inline : bool -> Libnames.qualid list -> unit
val print_extraction_inline : unit -> Pp.t
val reset_extraction_inline : unit -> unit
val extract_constant_inline : bool -> Libnames.qualid -> string list -> string -> unit
val extract_inductive : Libnames.qualid -> string -> string list -> string option -> unit
type int_or_id =
  1. | ArgInt of int
  2. | ArgId of Names.Id.t
val extraction_implicit : Libnames.qualid -> int_or_id list -> unit
val extraction_blacklist : Names.Id.t list -> unit
val reset_extraction_blacklist : unit -> unit
val print_extraction_blacklist : unit -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct