package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Extraction_plugin.TableSource

module Refset' : CSig.USetS with type elt = Names.GlobRef.t
Sourceval safe_basename_of_global : Names.GlobRef.t -> Names.Id.t
Sourceval warning_axioms : unit -> unit
Sourceval warning_opaques : bool -> unit
Sourceval warning_ambiguous_name : ?loc:Loc.t -> (Libnames.qualid * Names.ModPath.t * Names.GlobRef.t) -> unit
Sourceval warning_id : string -> unit
Sourceval error_axiom_scheme : ?loc:Loc.t -> Names.GlobRef.t -> int -> 'a
Sourceval error_constant : ?loc:Loc.t -> Names.GlobRef.t -> 'a
Sourceval error_inductive : ?loc:Loc.t -> Names.GlobRef.t -> 'a
Sourceval error_nb_cons : unit -> 'a
Sourceval error_module_clash : Names.ModPath.t -> Names.ModPath.t -> 'a
Sourceval error_no_module_expr : Names.ModPath.t -> 'a
Sourceval error_singleton_become_prop : Names.Id.t -> Names.GlobRef.t option -> 'a
Sourceval error_unknown_module : ?loc:Loc.t -> Libnames.qualid -> 'a
Sourceval error_scheme : unit -> 'a
Sourceval error_not_visible : Names.GlobRef.t -> 'a
Sourceval error_MPfile_as_mod : Names.ModPath.t -> bool -> 'a
Sourceval check_inside_section : unit -> unit
Sourceval check_loaded_modfile : Names.ModPath.t -> unit
Sourceval msg_of_implicit : Miniml.kill_reason -> string
Sourceval err_or_warn_remaining_implicit : Miniml.kill_reason -> unit
Sourceval info_file : string -> unit
Sourceval occur_kn_in_ref : Names.MutInd.t -> Names.GlobRef.t -> bool
Sourceval is_modfile : Names.ModPath.t -> bool
Sourceval string_of_modfile : Names.ModPath.t -> string
Sourceval file_of_modfile : Names.ModPath.t -> string
Sourceval is_toplevel : Names.ModPath.t -> bool
Sourceval at_toplevel : Names.ModPath.t -> bool
Sourceval mp_length : Names.ModPath.t -> int
Sourceval common_prefix_from_list : Names.ModPath.t -> Names.ModPath.t list -> Names.ModPath.t option
Sourceval get_nth_label_mp : int -> Names.ModPath.t -> Names.Label.t
Sourceval add_inductive_kind : Names.MutInd.t -> Miniml.inductive_kind -> unit
Sourceval is_coinductive : Names.GlobRef.t -> bool
Sourceval is_coinductive_type : Miniml.ml_type -> bool
Sourceval get_record_fields : Names.GlobRef.t -> Names.GlobRef.t option list
Sourceval record_fields_of_type : Miniml.ml_type -> Names.GlobRef.t option list
Sourceval add_recursors : Environ.env -> Names.MutInd.t -> unit
Sourceval is_recursor : Names.GlobRef.t -> bool
Sourceval add_projection : int -> Names.Constant.t -> Names.inductive -> unit
Sourceval is_projection : Names.GlobRef.t -> bool
Sourceval projection_arity : Names.GlobRef.t -> int
Sourceval projection_info : Names.GlobRef.t -> Names.inductive * int
Sourceval add_info_axiom : Names.GlobRef.t -> unit
Sourceval remove_info_axiom : Names.GlobRef.t -> unit
Sourceval add_log_axiom : Names.GlobRef.t -> unit
Sourceval add_symbol : Names.GlobRef.t -> unit
Sourceval add_symbol_rule : Names.GlobRef.t -> Names.Label.t -> unit
Sourceval add_opaque : Names.GlobRef.t -> unit
Sourceval remove_opaque : Names.GlobRef.t -> unit
Sourceval reset_tables : unit -> unit
Sourceval output_directory : unit -> string
Sourceval access_opaque : unit -> bool
Sourceval auto_inline : unit -> bool
Sourceval type_expand : unit -> bool
Sourceval keep_singleton : unit -> bool
Sourcetype 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;
}
Sourceval optims : unit -> opt_flag
Sourceval conservative_types : unit -> bool
Sourceval file_comment : unit -> string
Sourcetype lang =
  1. | Ocaml
  2. | Haskell
  3. | Scheme
  4. | JSON
Sourceval lang : unit -> lang
Sourceval set_modular : bool -> unit
Sourceval modular : unit -> bool
Sourceval set_library : bool -> unit
Sourceval library : unit -> bool
Sourceval set_extrcompute : bool -> unit
Sourceval is_extrcompute : unit -> bool
Sourceval to_inline : Names.GlobRef.t -> bool
Sourceval to_keep : Names.GlobRef.t -> bool
Sourceval implicits_of_global : Names.GlobRef.t -> Int.Set.t
Sourceval type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
Sourceval is_custom : Names.GlobRef.t -> bool
Sourceval is_inline_custom : Names.GlobRef.t -> bool
Sourceval is_foreign_custom : Names.GlobRef.t -> bool
Sourceval find_callback : Names.GlobRef.t -> string option
Sourceval find_custom : Names.GlobRef.t -> string
Sourceval find_type_custom : Names.GlobRef.t -> string list * string
Sourceval is_custom_match : Miniml.ml_branch array -> bool
Sourceval find_custom_match : Miniml.ml_branch array -> string
Sourceval extraction_language : lang -> unit
Sourceval extraction_inline : bool -> Libnames.qualid list -> unit
Sourceval print_extraction_inline : unit -> Pp.t
Sourceval print_extraction_foreign : unit -> Pp.t
Sourceval print_extraction_callback : unit -> Pp.t
Sourceval reset_extraction_inline : unit -> unit
Sourceval reset_extraction_foreign : unit -> unit
Sourceval reset_extraction_callback : unit -> unit
Sourceval extract_callback : string option -> Libnames.qualid -> unit
Sourceval extract_constant_inline : bool -> Libnames.qualid -> string list -> string -> unit
Sourceval extract_constant_foreign : Libnames.qualid -> string -> unit
Sourceval extract_inductive : Libnames.qualid -> string -> string list -> string option -> unit
Sourcetype int_or_id =
  1. | ArgInt of int
  2. | ArgId of Names.Id.t
Sourceval extraction_implicit : Libnames.qualid -> int_or_id list -> unit
Sourceval extraction_blacklist : string list -> unit
Sourceval reset_extraction_blacklist : unit -> unit
Sourceval 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