Module `Extraction_plugin.Table`Source

module Refset' : CSig.SetS with type elt = Names.GlobRef.t

Sourcemodule Refmap' : CSig.MapS with type key = Names.GlobRef.t

Sourceval safe_basename_of_global : Names.GlobRef.t -> Names.Id.t

Sourceval warning_axioms : unit -> unit

Sourceval warning_opaques : bool -> unit

val 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_module : unit -> unit

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 repr_of_r : Names.GlobRef.t -> Names.KerName.t

Sourceval modpath_of_r : Names.GlobRef.t -> Names.ModPath.t

Sourceval label_of_r : Names.GlobRef.t -> Names.Label.t

Sourceval base_mp : Names.ModPath.t -> Names.ModPath.t

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 prefixes_mp : Names.ModPath.t -> Names.MPset.t

Source

val 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 labels_of_ref : Names.GlobRef.t -> Names.ModPath.t * Names.Label.t list

Source

val add_typedef : 
  Names.Constant.t ->
  Declarations.constant_body ->
  Miniml.ml_type ->
  unit

Source

val lookup_typedef : 
  Names.Constant.t ->
  Declarations.constant_body ->
  Miniml.ml_type option

Source

val add_cst_type : 
  Names.Constant.t ->
  Declarations.constant_body ->
  Miniml.ml_schema ->
  unit

Source

val lookup_cst_type : 
  Names.Constant.t ->
  Declarations.constant_body ->
  Miniml.ml_schema option

Source

val add_ind : 
  Names.MutInd.t ->
  Declarations.mutual_inductive_body ->
  Miniml.ml_ind ->
  unit

Source

val lookup_ind : 
  Names.MutInd.t ->
  Declarations.mutual_inductive_body ->
  Miniml.ml_ind option

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_opaque : Names.GlobRef.t -> unit

Sourceval remove_opaque : Names.GlobRef.t -> unit

Sourceval reset_tables : unit -> unit

Sourceval access_opaque : unit -> bool

Sourceval auto_inline : unit -> bool

Sourceval type_expand : unit -> bool

Sourceval keep_singleton : unit -> bool

Sourcetype opt_flag = {

opt_kill_dum : bool;
opt_fix_fun : bool;
opt_case_iot : bool;
opt_case_idr : bool;
opt_case_idg : bool;
opt_case_cst : bool;
opt_case_fun : bool;
opt_case_app : bool;
opt_let_app : bool;
opt_lin_let : bool;
opt_lin_beta : bool;

}

Sourceval optims : unit -> opt_flag

Sourceval conservative_types : unit -> bool

Sourceval file_comment : unit -> string

Sourcetype lang =

| Ocaml
| Haskell
| Scheme
| 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 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 reset_extraction_inline : unit -> unit

Source

val extract_constant_inline : 
  bool ->
  Libnames.qualid ->
  string list ->
  string ->
  unit

Source

val extract_inductive : 
  Libnames.qualid ->
  string ->
  string list ->
  string option ->
  unit

Sourcetype int_or_id =

| ArgInt of int
| 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Table/index.html

Module `Extraction_plugin.Table`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Table/index.html

Module Extraction_plugin.TableSource

Module `Extraction_plugin.Table`Source