diff --git a/master/api/coq-core/Extraction_plugin/Table/index.html b/master/api/coq-core/Extraction_plugin/Table/index.html index e9594730c2..3272cce270 100644 --- a/master/api/coq-core/Extraction_plugin/Table/index.html +++ b/master/api/coq-core/Extraction_plugin/Table/index.html @@ -1,2 +1,2 @@ -Table (coq-core.Extraction_plugin.Table)

Module Extraction_plugin.Table

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_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 repr_of_r : Names.GlobRef.t -> Names.KerName.t
val modpath_of_r : Names.GlobRef.t -> Names.ModPath.t
val label_of_r : Names.GlobRef.t -> Names.Label.t
val base_mp : Names.ModPath.t -> Names.ModPath.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_typedef : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_type -> unit
val lookup_typedef : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_type option
val add_cst_type : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_schema -> unit
val lookup_cst_type : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_schema option
val add_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Miniml.ml_ind -> unit
val lookup_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Miniml.ml_ind option
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 = {
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;
}
val optims : unit -> opt_flag
val conservative_types : unit -> bool
val file_comment : unit -> string
type lang =
| Ocaml
| Haskell
| Scheme
| 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 =
| ArgInt of int
| ArgId of Names.Id.t
val extraction_implicit : Libnames.qualid -> int_or_id list -> unit
val extraction_blacklist : string list -> unit
val reset_extraction_blacklist : unit -> unit
val print_extraction_blacklist : unit -> Pp.t
\ No newline at end of file +Table (coq-core.Extraction_plugin.Table)

Module Extraction_plugin.Table

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_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 repr_of_r : Names.GlobRef.t -> Names.KerName.t
val modpath_of_r : Names.GlobRef.t -> Names.ModPath.t
val label_of_r : Names.GlobRef.t -> Names.Label.t
val base_mp : Names.ModPath.t -> Names.ModPath.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_typedef : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_type -> unit
val lookup_typedef : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_type option
val add_cst_type : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_schema -> unit
val lookup_cst_type : Names.Constant.t -> Declarations.constant_body -> Miniml.ml_schema option
val add_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Miniml.ml_ind -> unit
val lookup_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Miniml.ml_ind option
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 output_directory : unit -> string
val access_opaque : unit -> bool
val auto_inline : unit -> bool
val type_expand : unit -> bool
val keep_singleton : unit -> bool
type 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;
}
val optims : unit -> opt_flag
val conservative_types : unit -> bool
val file_comment : unit -> string
type lang =
| Ocaml
| Haskell
| Scheme
| 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 =
| ArgInt of int
| ArgId of Names.Id.t
val extraction_implicit : Libnames.qualid -> int_or_id list -> unit
val extraction_blacklist : string list -> unit
val reset_extraction_blacklist : unit -> unit
val print_extraction_blacklist : unit -> Pp.t
\ No newline at end of file diff --git a/master/api/coq-core/Extraction_plugin__Table/index.html b/master/api/coq-core/Extraction_plugin__Table/index.html index bf68ef41cd..d68db07d70 100644 --- a/master/api/coq-core/Extraction_plugin__Table/index.html +++ b/master/api/coq-core/Extraction_plugin__Table/index.html @@ -1,2 +1,2 @@ -Extraction_plugin__Table (coq-core.Extraction_plugin__Table)

Module Extraction_plugin__Table

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_section : unit -> unit
val check_loaded_modfile : Names.ModPath.t -> unit
val msg_of_implicit : Extraction_plugin.Miniml.kill_reason -> string
val err_or_warn_remaining_implicit : Extraction_plugin.Miniml.kill_reason -> unit
val info_file : string -> unit
val occur_kn_in_ref : Names.MutInd.t -> Names.GlobRef.t -> bool
val repr_of_r : Names.GlobRef.t -> Names.KerName.t
val modpath_of_r : Names.GlobRef.t -> Names.ModPath.t
val label_of_r : Names.GlobRef.t -> Names.Label.t
val base_mp : Names.ModPath.t -> Names.ModPath.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_typedef : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_type -> unit
val lookup_typedef : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_type option
val add_cst_type : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_schema -> unit
val lookup_cst_type : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_schema option
val add_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Extraction_plugin.Miniml.ml_ind -> unit
val lookup_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Extraction_plugin.Miniml.ml_ind option
val add_inductive_kind : Names.MutInd.t -> Extraction_plugin.Miniml.inductive_kind -> unit
val is_coinductive : Names.GlobRef.t -> bool
val is_coinductive_type : Extraction_plugin.Miniml.ml_type -> bool
val get_record_fields : Names.GlobRef.t -> Names.GlobRef.t option list
val record_fields_of_type : Extraction_plugin.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 = {
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;
}
val optims : unit -> opt_flag
val conservative_types : unit -> bool
val file_comment : unit -> string
type lang =
| Ocaml
| Haskell
| Scheme
| 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 : Extraction_plugin.Miniml.ml_branch array -> bool
val find_custom_match : Extraction_plugin.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 =
| ArgInt of int
| ArgId of Names.Id.t
val extraction_implicit : Libnames.qualid -> int_or_id list -> unit
val extraction_blacklist : string list -> unit
val reset_extraction_blacklist : unit -> unit
val print_extraction_blacklist : unit -> Pp.t
\ No newline at end of file +Extraction_plugin__Table (coq-core.Extraction_plugin__Table)

Module Extraction_plugin__Table

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_section : unit -> unit
val check_loaded_modfile : Names.ModPath.t -> unit
val msg_of_implicit : Extraction_plugin.Miniml.kill_reason -> string
val err_or_warn_remaining_implicit : Extraction_plugin.Miniml.kill_reason -> unit
val info_file : string -> unit
val occur_kn_in_ref : Names.MutInd.t -> Names.GlobRef.t -> bool
val repr_of_r : Names.GlobRef.t -> Names.KerName.t
val modpath_of_r : Names.GlobRef.t -> Names.ModPath.t
val label_of_r : Names.GlobRef.t -> Names.Label.t
val base_mp : Names.ModPath.t -> Names.ModPath.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_typedef : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_type -> unit
val lookup_typedef : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_type option
val add_cst_type : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_schema -> unit
val lookup_cst_type : Names.Constant.t -> Declarations.constant_body -> Extraction_plugin.Miniml.ml_schema option
val add_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Extraction_plugin.Miniml.ml_ind -> unit
val lookup_ind : Names.MutInd.t -> Declarations.mutual_inductive_body -> Extraction_plugin.Miniml.ml_ind option
val add_inductive_kind : Names.MutInd.t -> Extraction_plugin.Miniml.inductive_kind -> unit
val is_coinductive : Names.GlobRef.t -> bool
val is_coinductive_type : Extraction_plugin.Miniml.ml_type -> bool
val get_record_fields : Names.GlobRef.t -> Names.GlobRef.t option list
val record_fields_of_type : Extraction_plugin.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 output_directory : unit -> string
val access_opaque : unit -> bool
val auto_inline : unit -> bool
val type_expand : unit -> bool
val keep_singleton : unit -> bool
type 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;
}
val optims : unit -> opt_flag
val conservative_types : unit -> bool
val file_comment : unit -> string
type lang =
| Ocaml
| Haskell
| Scheme
| 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 : Extraction_plugin.Miniml.ml_branch array -> bool
val find_custom_match : Extraction_plugin.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 =
| ArgInt of int
| ArgId of Names.Id.t
val extraction_implicit : Libnames.qualid -> int_or_id list -> unit
val extraction_blacklist : string list -> unit
val reset_extraction_blacklist : unit -> unit
val print_extraction_blacklist : unit -> Pp.t
\ No newline at end of file diff --git a/master/api/coq-core/System/index.html b/master/api/coq-core/System/index.html index ad44a82167..4faa3684fa 100644 --- a/master/api/coq-core/System/index.html +++ b/master/api/coq-core/System/index.html @@ -1,2 +1,2 @@ -System (coq-core.System)

Module System

Coqtop specific system utilities
Directories
type unix_path = string
type file_kind =
| FileDir of unix_path * string
| FileRegular of string
val (//) : unix_path -> string -> unix_path
val exists_dir : unix_path -> bool
val exclude_directory : unix_path -> unit
val process_directory : (file_kind -> unit) -> unix_path -> unit
val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
Files and load paths
val warn_cannot_open_dir : ?⁠loc:Loc.t -> string -> unit
val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
val is_in_path : CUnix.load_path -> string -> bool
val is_in_system_path : string -> bool
val where_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
val find_file_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string

find_file_in_path ?warn loadpath filename returns the directory name and long name of the first physical occurrence filename in one of the directory of the loadpath; fails with a user error if no such file exists; warn if two or more files exist in the loadpath; returns instead the directory name of filename is filename is an absolute path

val all_in_path : (CUnix.physical_path * 'a) list -> string -> ('a * string) list

all_in_path loadpath filename returns the list of the directory name and full name of all physical occurrences of filename in a loadpath binding physical paths to some arbitrary key

val trust_file_cache : bool Stdlib.ref

trust_file_cache indicates whether we trust the underlying mapped file-system not to change along the execution of Coq. This assumption greatly speds up file search, but it is often inconvenient in interactive mode

val file_exists_respecting_case : string -> string -> bool
I/O functions
type magic_number_error = {
filename : string;
actual : int32;
expected : int32;
}
exception Bad_magic_number of magic_number_error
exception Bad_version_number of magic_number_error
val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
val input_int32 : Stdlib.in_channel -> int32
val input_int64 : Stdlib.in_channel -> int64
val output_int32 : Stdlib.out_channel -> int32 -> unit
val output_int64 : Stdlib.out_channel -> int64 -> unit
val marshal_out : Stdlib.out_channel -> 'a -> unit
val marshal_in : string -> Stdlib.in_channel -> 'a
val check_caml_version : caml:string -> file:string -> unit
Time stamps.
type time
type duration
val get_time : unit -> time
val time_difference : time -> time -> float

in seconds

val duration_between : start:time -> stop:time -> duration
val duration_add : duration -> duration -> duration
val duration_real : duration -> float
val fmt_time_difference : time -> time -> Pp.t
val fmt_duration : duration -> Pp.t
type 'a transaction_result = ('a * duration, Exninfo.iexn * duration) Stdlib.Result.t
val measure_duration : ('a -> 'b) -> 'a -> 'b transaction_result
val fmt_transaction_result : 'a transaction_result -> Pp.t
Instruction count.
type instruction_count = (Stdlib.Int64.t, string) Stdlib.Result.t
val instructions_between : c_start:instruction_count -> c_end:instruction_count -> instruction_count
val instruction_count_add : instruction_count -> instruction_count -> instruction_count
type 'a instructions_result = ('a * instruction_count, Exninfo.iexn * instruction_count) Stdlib.Result.t
val count_instructions : ('a -> 'b) -> 'a -> 'b instructions_result
val fmt_instructions_result : 'a instructions_result -> Pp.t
val get_toplevel_path : ?⁠byte:bool -> string -> string

get_toplevel_path program builds a complete path to the executable denoted by program. This involves:

  • locating the directory: we don't rely on PATH as to make calls to /foo/bin/coqtop chose the right /foo/bin/coqproofworker
  • adding the proper suffixes: .opt/.byte depending on the current mode, + .exe if in windows.

Note that this function doesn't check that the executable actually exists. This is left back to caller, as well as the choice of fallback strategy. We could add a fallback strategy here but it is better not to as in most cases if this function fails to construct the right name you want you execution to fail rather than fall into choosing some random binary from the system-wide installation of Coq.

\ No newline at end of file +System (coq-core.System)

Module System

Coqtop specific system utilities
Directories
type unix_path = string
type file_kind =
| FileDir of unix_path * string
| FileRegular of string
val (//) : unix_path -> string -> unix_path
val exists_dir : unix_path -> bool
val mkdir : unix_path -> unit
val exclude_directory : unix_path -> unit
val process_directory : (file_kind -> unit) -> unix_path -> unit
val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
Files and load paths
val warn_cannot_open_dir : ?⁠loc:Loc.t -> string -> unit
val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
val is_in_path : CUnix.load_path -> string -> bool
val is_in_system_path : string -> bool
val where_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
val find_file_in_path : ?⁠warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string

find_file_in_path ?warn loadpath filename returns the directory name and long name of the first physical occurrence filename in one of the directory of the loadpath; fails with a user error if no such file exists; warn if two or more files exist in the loadpath; returns instead the directory name of filename is filename is an absolute path

val all_in_path : (CUnix.physical_path * 'a) list -> string -> ('a * string) list

all_in_path loadpath filename returns the list of the directory name and full name of all physical occurrences of filename in a loadpath binding physical paths to some arbitrary key

val trust_file_cache : bool Stdlib.ref

trust_file_cache indicates whether we trust the underlying mapped file-system not to change along the execution of Coq. This assumption greatly speds up file search, but it is often inconvenient in interactive mode

val file_exists_respecting_case : string -> string -> bool
I/O functions
type magic_number_error = {
filename : string;
actual : int32;
expected : int32;
}
exception Bad_magic_number of magic_number_error
exception Bad_version_number of magic_number_error
val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
val input_int32 : Stdlib.in_channel -> int32
val input_int64 : Stdlib.in_channel -> int64
val output_int32 : Stdlib.out_channel -> int32 -> unit
val output_int64 : Stdlib.out_channel -> int64 -> unit
val marshal_out : Stdlib.out_channel -> 'a -> unit
val marshal_in : string -> Stdlib.in_channel -> 'a
val check_caml_version : caml:string -> file:string -> unit
Time stamps.
type time
type duration
val get_time : unit -> time
val time_difference : time -> time -> float

in seconds

val duration_between : start:time -> stop:time -> duration
val duration_add : duration -> duration -> duration
val duration_real : duration -> float
val fmt_time_difference : time -> time -> Pp.t
val fmt_duration : duration -> Pp.t
type 'a transaction_result = ('a * duration, Exninfo.iexn * duration) Stdlib.Result.t
val measure_duration : ('a -> 'b) -> 'a -> 'b transaction_result
val fmt_transaction_result : 'a transaction_result -> Pp.t
Instruction count.
type instruction_count = (Stdlib.Int64.t, string) Stdlib.Result.t
val instructions_between : c_start:instruction_count -> c_end:instruction_count -> instruction_count
val instruction_count_add : instruction_count -> instruction_count -> instruction_count
type 'a instructions_result = ('a * instruction_count, Exninfo.iexn * instruction_count) Stdlib.Result.t
val count_instructions : ('a -> 'b) -> 'a -> 'b instructions_result
val fmt_instructions_result : 'a instructions_result -> Pp.t
val get_toplevel_path : ?⁠byte:bool -> string -> string

get_toplevel_path program builds a complete path to the executable denoted by program. This involves:

  • locating the directory: we don't rely on PATH as to make calls to /foo/bin/coqtop chose the right /foo/bin/coqproofworker
  • adding the proper suffixes: .opt/.byte depending on the current mode, + .exe if in windows.

Note that this function doesn't check that the executable actually exists. This is left back to caller, as well as the choice of fallback strategy. We could add a fallback strategy here but it is better not to as in most cases if this function fails to construct the right name you want you execution to fail rather than fall into choosing some random binary from the system-wide installation of Coq.

\ No newline at end of file diff --git a/master/refman/.doctrees/addendum/extraction.doctree b/master/refman/.doctrees/addendum/extraction.doctree index 38f0a8aa65..7288920f70 100644 Binary files a/master/refman/.doctrees/addendum/extraction.doctree and b/master/refman/.doctrees/addendum/extraction.doctree differ diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree index f8b727b17c..71a79c4532 100644 Binary files a/master/refman/.doctrees/addendum/generalized-rewriting.doctree and b/master/refman/.doctrees/addendum/generalized-rewriting.doctree differ diff --git a/master/refman/.doctrees/addendum/implicit-coercions.doctree b/master/refman/.doctrees/addendum/implicit-coercions.doctree index 8ef3f9b000..9c3329a30d 100644 Binary files a/master/refman/.doctrees/addendum/implicit-coercions.doctree and b/master/refman/.doctrees/addendum/implicit-coercions.doctree differ diff --git a/master/refman/.doctrees/addendum/micromega.doctree b/master/refman/.doctrees/addendum/micromega.doctree index 92d2587be2..a1119986e1 100644 Binary files a/master/refman/.doctrees/addendum/micromega.doctree and b/master/refman/.doctrees/addendum/micromega.doctree differ diff --git a/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree b/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree index 70d13a05b6..b7541f548d 100644 Binary files a/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree and b/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree differ diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree index e653babfb3..52b0937e75 100644 Binary files a/master/refman/.doctrees/addendum/program.doctree and b/master/refman/.doctrees/addendum/program.doctree differ diff --git a/master/refman/.doctrees/addendum/ring.doctree b/master/refman/.doctrees/addendum/ring.doctree index 8a0522e50d..13886c9511 100644 Binary files a/master/refman/.doctrees/addendum/ring.doctree and b/master/refman/.doctrees/addendum/ring.doctree differ diff --git a/master/refman/.doctrees/addendum/sprop.doctree b/master/refman/.doctrees/addendum/sprop.doctree index cfc76aaf7d..485c78df5d 100644 Binary files a/master/refman/.doctrees/addendum/sprop.doctree and b/master/refman/.doctrees/addendum/sprop.doctree differ diff --git a/master/refman/.doctrees/addendum/type-classes.doctree b/master/refman/.doctrees/addendum/type-classes.doctree index 7b3ae742e0..680b40dcc4 100644 Binary files a/master/refman/.doctrees/addendum/type-classes.doctree and b/master/refman/.doctrees/addendum/type-classes.doctree differ diff --git a/master/refman/.doctrees/addendum/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree index 416dbf9595..7ca917259e 100644 Binary files a/master/refman/.doctrees/addendum/universe-polymorphism.doctree and b/master/refman/.doctrees/addendum/universe-polymorphism.doctree differ diff --git a/master/refman/.doctrees/changes.doctree b/master/refman/.doctrees/changes.doctree index c415fd6b92..0e821dce05 100644 Binary files a/master/refman/.doctrees/changes.doctree and b/master/refman/.doctrees/changes.doctree differ diff --git a/master/refman/.doctrees/environment.pickle b/master/refman/.doctrees/environment.pickle index 5d7a98cb5e..2103e41a83 100644 Binary files a/master/refman/.doctrees/environment.pickle and b/master/refman/.doctrees/environment.pickle differ diff --git a/master/refman/.doctrees/language/cic.doctree b/master/refman/.doctrees/language/cic.doctree index 2911f4e43a..5edae4e165 100644 Binary files a/master/refman/.doctrees/language/cic.doctree and b/master/refman/.doctrees/language/cic.doctree differ diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree index 1e93e51054..b17b7c60af 100644 Binary files a/master/refman/.doctrees/language/coq-library.doctree and b/master/refman/.doctrees/language/coq-library.doctree differ diff --git a/master/refman/.doctrees/language/core/assumptions.doctree b/master/refman/.doctrees/language/core/assumptions.doctree index 67e18f0740..755dbdafcf 100644 Binary files a/master/refman/.doctrees/language/core/assumptions.doctree and b/master/refman/.doctrees/language/core/assumptions.doctree differ diff --git a/master/refman/.doctrees/language/core/basic.doctree b/master/refman/.doctrees/language/core/basic.doctree index a1525583e1..b787420bef 100644 Binary files a/master/refman/.doctrees/language/core/basic.doctree and b/master/refman/.doctrees/language/core/basic.doctree differ diff --git a/master/refman/.doctrees/language/core/coinductive.doctree b/master/refman/.doctrees/language/core/coinductive.doctree index 5eb9830e1c..2b6d091dfb 100644 Binary files a/master/refman/.doctrees/language/core/coinductive.doctree and b/master/refman/.doctrees/language/core/coinductive.doctree differ diff --git a/master/refman/.doctrees/language/core/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree index fe2ed1f2af..8e24ef1384 100644 Binary files a/master/refman/.doctrees/language/core/conversion.doctree and b/master/refman/.doctrees/language/core/conversion.doctree differ diff --git a/master/refman/.doctrees/language/core/inductive.doctree b/master/refman/.doctrees/language/core/inductive.doctree index 62592c09e0..03967660e1 100644 Binary files a/master/refman/.doctrees/language/core/inductive.doctree and b/master/refman/.doctrees/language/core/inductive.doctree differ diff --git a/master/refman/.doctrees/language/core/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree index d8dd82cda2..e4fda4d7bf 100644 Binary files a/master/refman/.doctrees/language/core/modules.doctree and b/master/refman/.doctrees/language/core/modules.doctree differ diff --git a/master/refman/.doctrees/language/core/primitive.doctree b/master/refman/.doctrees/language/core/primitive.doctree index 02242468d7..f38a05beee 100644 Binary files a/master/refman/.doctrees/language/core/primitive.doctree and b/master/refman/.doctrees/language/core/primitive.doctree differ diff --git a/master/refman/.doctrees/language/core/records.doctree b/master/refman/.doctrees/language/core/records.doctree index 6fa692da0d..a9c0191e62 100644 Binary files a/master/refman/.doctrees/language/core/records.doctree and b/master/refman/.doctrees/language/core/records.doctree differ diff --git a/master/refman/.doctrees/language/core/sections.doctree b/master/refman/.doctrees/language/core/sections.doctree index f3f02d993e..81c5eee342 100644 Binary files a/master/refman/.doctrees/language/core/sections.doctree and b/master/refman/.doctrees/language/core/sections.doctree differ diff --git a/master/refman/.doctrees/language/core/variants.doctree b/master/refman/.doctrees/language/core/variants.doctree index 3f1a44dbaf..974174c244 100644 Binary files a/master/refman/.doctrees/language/core/variants.doctree and b/master/refman/.doctrees/language/core/variants.doctree differ diff --git a/master/refman/.doctrees/language/extensions/arguments-command.doctree b/master/refman/.doctrees/language/extensions/arguments-command.doctree index 49327d726e..404a91c362 100644 Binary files a/master/refman/.doctrees/language/extensions/arguments-command.doctree and b/master/refman/.doctrees/language/extensions/arguments-command.doctree differ diff --git a/master/refman/.doctrees/language/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree index 64f619ab94..d641d3a0d0 100644 Binary files a/master/refman/.doctrees/language/extensions/canonical.doctree and b/master/refman/.doctrees/language/extensions/canonical.doctree differ diff --git a/master/refman/.doctrees/language/extensions/evars.doctree b/master/refman/.doctrees/language/extensions/evars.doctree index cad6560791..762682b040 100644 Binary files a/master/refman/.doctrees/language/extensions/evars.doctree and b/master/refman/.doctrees/language/extensions/evars.doctree differ diff --git a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree index b7d4ac0ba5..4a4e6f01ae 100644 Binary files a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree and b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree differ diff --git a/master/refman/.doctrees/language/extensions/match.doctree b/master/refman/.doctrees/language/extensions/match.doctree index 70363a1ef2..c05739d1e8 100644 Binary files a/master/refman/.doctrees/language/extensions/match.doctree and b/master/refman/.doctrees/language/extensions/match.doctree differ diff --git a/master/refman/.doctrees/practical-tools/coq-commands.doctree b/master/refman/.doctrees/practical-tools/coq-commands.doctree index 4b2b1c0765..5b3e163e57 100644 Binary files a/master/refman/.doctrees/practical-tools/coq-commands.doctree and b/master/refman/.doctrees/practical-tools/coq-commands.doctree differ diff --git a/master/refman/.doctrees/practical-tools/coqide.doctree b/master/refman/.doctrees/practical-tools/coqide.doctree index 2a784f484a..5102c58a1b 100644 Binary files a/master/refman/.doctrees/practical-tools/coqide.doctree and b/master/refman/.doctrees/practical-tools/coqide.doctree differ diff --git a/master/refman/.doctrees/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree index 037826515f..6443ca27be 100644 Binary files a/master/refman/.doctrees/proof-engine/ltac.doctree and b/master/refman/.doctrees/proof-engine/ltac.doctree differ diff --git a/master/refman/.doctrees/proof-engine/ltac2.doctree b/master/refman/.doctrees/proof-engine/ltac2.doctree index 739ee7aa61..d917a009ff 100644 Binary files a/master/refman/.doctrees/proof-engine/ltac2.doctree and b/master/refman/.doctrees/proof-engine/ltac2.doctree differ diff --git a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree index 033853895a..372844f31f 100644 Binary files a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree and b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree differ diff --git a/master/refman/.doctrees/proof-engine/tactics.doctree b/master/refman/.doctrees/proof-engine/tactics.doctree index 51d2e13907..97d57a1d3f 100644 Binary files a/master/refman/.doctrees/proof-engine/tactics.doctree and b/master/refman/.doctrees/proof-engine/tactics.doctree differ diff --git a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree index 68045e3009..8492151b0d 100644 Binary files a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree and b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree differ diff --git a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree index 3a7f7467a6..57a956a681 100644 Binary files a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree and b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree differ diff --git a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree index 90723d00b0..a6398aaca0 100644 Binary files a/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree and b/master/refman/.doctrees/proofs/automatic-tactics/logic.doctree differ diff --git a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree index 6d57ec86a5..b995986e65 100644 Binary files a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree and b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree differ diff --git a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree index 4aa74e0568..b2e3ac5127 100644 Binary files a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree and b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree differ diff --git a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree index ea06952e20..56e79af5b4 100644 Binary files a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree and b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree differ diff --git a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree index c72eca40aa..dd4c1f65d2 100644 Binary files a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree and b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree differ diff --git a/master/refman/.doctrees/using/libraries/funind.doctree b/master/refman/.doctrees/using/libraries/funind.doctree index 6b38d77ef1..c30234e3ca 100644 Binary files a/master/refman/.doctrees/using/libraries/funind.doctree and b/master/refman/.doctrees/using/libraries/funind.doctree differ diff --git a/master/refman/.doctrees/using/libraries/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree index 712a856142..be06af90fb 100644 Binary files a/master/refman/.doctrees/using/libraries/writing.doctree and b/master/refman/.doctrees/using/libraries/writing.doctree differ diff --git a/master/refman/_sources/addendum/extraction.rst.txt b/master/refman/_sources/addendum/extraction.rst.txt index 22587fbc1c..de8887195c 100644 --- a/master/refman/_sources/addendum/extraction.rst.txt +++ b/master/refman/_sources/addendum/extraction.rst.txt @@ -485,6 +485,11 @@ Additional settings If this :term:`flag` is set, fully expand Coq types in ML. See the Coq source code to learn more. +.. opt:: Extraction Output Directory @string + + Sets the directory where extracted files will be written. + The default is the current directory, which can be displayed with :cmd:`Pwd`. + Differences between Coq and ML type systems ---------------------------------------------- diff --git a/master/refman/_sources/practical-tools/coq-commands.rst.txt b/master/refman/_sources/practical-tools/coq-commands.rst.txt index c0cf41638d..00c0160081 100644 --- a/master/refman/_sources/practical-tools/coq-commands.rst.txt +++ b/master/refman/_sources/practical-tools/coq-commands.rst.txt @@ -363,7 +363,7 @@ and ``coqtop``, unless stated otherwise: - none - none -:-native-output-dir: Set the directory in which to put the aforementioned +:-native-output-dir *dir*: Set the directory in which to put the aforementioned ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``. :-vos: Indicate Coq to skip the processing of opaque proofs (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files diff --git a/master/refman/addendum/canonical-structures.html b/master/refman/addendum/canonical-structures.html index 9ae3071e18..8acdfcbc54 100644 --- a/master/refman/addendum/canonical-structures.html +++ b/master/refman/addendum/canonical-structures.html @@ -979,32 +979,32 @@
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0
  • Version 8.17
  • Version 8.16
  • Version 8.15
  • Version 8.14
  • Version 8.13
  • Version 8.12
  • Version 8.11
  • Version 8.10
  • Version 8.9
  • Version 8.8
  • Version 8.7
  • Version 8.6
  • Version 8.5
  • Version 8.4
  • Version 8.3
  • Version 8.2
  • Version 8.1
  • Version 8.0