diff --git a/master/api/coq-core/DeclareUniv/index.html b/master/api/coq-core/DeclareUniv/index.html index ebf7ecb85f..550bc77b20 100644 --- a/master/api/coq-core/DeclareUniv/index.html +++ b/master/api/coq-core/DeclareUniv/index.html @@ -1,2 +1,2 @@ -
DeclareUniv
exception AlreadyDeclared of string option * Names.Id.t
Also used by Declare
for constants, DeclareInd
for inductives, etc. Containts object_kind , id
.
val declare_univ_binders : Names.GlobRef.t -> UState.named_universes_entry -> unit
Internally used to declare names of universes from monomorphic constants/inductives. Noop on polymorphic references.
val do_universe : poly:bool -> Names.lident list -> unit
Command Universes
.
val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
Command Constraint
.
val add_constraint_source : Names.GlobRef.t -> Univ.ContextSet.t -> unit
val constraint_sources : unit -> (Names.GlobRef.t * Univ.Constraints.t) list
Returns constraints associated to globrefs, newest first.
DeclareUniv
exception AlreadyDeclared of string option * Names.Id.t
Also used by Declare
for constants, DeclareInd
for inductives, etc. Containts object_kind , id
.
val declare_univ_binders : Names.GlobRef.t -> UState.named_universes_entry -> unit
Internally used to declare names of universes from monomorphic constants/inductives. Noop on polymorphic references.
val name_mono_section_univs : Univ.Level.Set.t -> unit
Internally used to name universes associated with no particular constant in a section.
val do_universe : poly:bool -> Names.lident list -> unit
Command Universes
.
val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
Command Constraint
.
val add_constraint_source : Names.GlobRef.t -> Univ.ContextSet.t -> unit
val constraint_sources : unit -> (Names.GlobRef.t * Univ.Constraints.t) list
Returns constraints associated to globrefs, newest first.
Lib.Interp
type summary = Summary.Interp.frozen
type classified_objects = {
substobjs : Libobject.t list; |
keepobjs : Libobject.t list; |
anticipateobjs : Libobject.t list; |
}
val classify_segment : Libobject.t list -> classified_objects
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Lib.Interp
type summary = Summary.Interp.frozen
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Lib.Synterp
type summary = Summary.Synterp.frozen
type classified_objects = {
substobjs : Libobject.t list; |
keepobjs : Libobject.t list; |
anticipateobjs : Libobject.t list; |
}
val classify_segment : Libobject.t list -> classified_objects
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Lib.Synterp
type summary = Summary.Synterp.frozen
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Lib
Lib: record of operations, backtrack, low-level sections
This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step).
type export = (export_flag * Libobject.open_filter) option
val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
val make_foname : Names.Id.t -> Libobject.object_name
val oname_prefix : Libobject.object_name -> Nametab.object_prefix
type 'summary node =
| CompilingLibrary of Nametab.object_prefix |
| OpenedModule of is_type * export * Nametab.object_prefix * 'summary |
| OpenedSection of Nametab.object_prefix * 'summary |
val node_prefix : 'summary node -> Nametab.object_prefix
Extract the object_prefix
component. Note that it is the prefix of the objects *inside* this node, eg in Module M.
we have OpenedModule
with prefix containing M
.
type 'summary library_segment = ('summary node * Libobject.t list) list
Adding operations (which call the cache
method, and getting the current list of operations (most recent ones coming first).
val add_leaf : Libobject.obj -> unit
val add_discharged_leaf : Libobject.discharged_obj -> unit
The function contents
gives access to the current entire segment
val contents : unit -> Summary.Interp.frozen library_segment
val prefix : unit -> Nametab.object_prefix
User-side names
cwd()
is (prefix()).obj_dir
current_mp()
is (prefix()).obj_mp
Inside a library A.B module M section S, we have
make_path (resp make_path_except_section) uses cwd (resp cwd_except_section) make_kn uses current_mp
val cwd : unit -> Names.DirPath.t
val cwd_except_section : unit -> Names.DirPath.t
val current_dirpath : bool -> Names.DirPath.t
val make_path : Names.Id.t -> Libnames.full_path
val make_path_except_section : Names.Id.t -> Libnames.full_path
val current_mp : unit -> Names.ModPath.t
Kernel-side names
val make_kn : Names.Id.t -> Names.KerName.t
type discharged_item =
| DischargedExport of Libobject.ExportObj.t |
| DischargedLeaf of Libobject.discharged_obj |
module type StagedLibS = sig ... end
The StagedLibS
abstraction describes operations and traversal for Lib at a given stage.
We provide two instances of StagedLibS
, corresponding to the Synterp and Interp stages.
module Synterp : StagedLibS with type summary = Summary.Synterp.frozen
module Interp : StagedLibS with type summary = Summary.Interp.frozen
val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
val end_compilation : Names.DirPath.t -> Nametab.object_prefix * Library_info.t * Interp.classified_objects * Synterp.classified_objects
Finalize the compilation of a library and return respectively the library prefix, the regular objects, and the syntax-related objects.
val library_dp : unit -> Names.DirPath.t
The function library_dp
returns the DirPath.t
of the current compiling library (or default_library
)
val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
Extract the library part of a name even if in a section
val library_part : Names.GlobRef.t -> Names.DirPath.t
val section_segment_of_constant : Names.Constant.t -> Cooking.cooking_info
Section management for discharge
val section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info
val section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info
val section_instance : Names.GlobRef.t -> Constr.t array
val is_in_section : Names.GlobRef.t -> bool
val discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t
discharge_proj_repr p
discharges projection p
if the associated record was defined in the current section. If that is not the case, it returns p
unchanged.
Compatibility layer
Lib
Lib: record of operations, backtrack, low-level sections
This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step).
type export = (export_flag * Libobject.open_filter) option
val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
val make_foname : Names.Id.t -> Libobject.object_name
val oname_prefix : Libobject.object_name -> Nametab.object_prefix
type 'summary node =
| CompilingLibrary of Nametab.object_prefix |
| OpenedModule of is_type * export * Nametab.object_prefix * 'summary |
| OpenedSection of Nametab.object_prefix * 'summary |
val node_prefix : 'summary node -> Nametab.object_prefix
Extract the object_prefix
component. Note that it is the prefix of the objects *inside* this node, eg in Module M.
we have OpenedModule
with prefix containing M
.
type 'summary library_segment = ('summary node * Libobject.t list) list
Adding operations (which call the cache
method, and getting the current list of operations (most recent ones coming first).
val add_leaf : Libobject.obj -> unit
val add_discharged_leaf : Libobject.discharged_obj -> unit
The function contents
gives access to the current entire segment
val contents : unit -> Summary.Interp.frozen library_segment
val prefix : unit -> Nametab.object_prefix
User-side names
cwd()
is (prefix()).obj_dir
current_mp()
is (prefix()).obj_mp
Inside a library A.B module M section S, we have
make_path (resp make_path_except_section) uses cwd (resp cwd_except_section) make_kn uses current_mp
val cwd : unit -> Names.DirPath.t
val cwd_except_section : unit -> Names.DirPath.t
val current_dirpath : bool -> Names.DirPath.t
val make_path : Names.Id.t -> Libnames.full_path
val make_path_except_section : Names.Id.t -> Libnames.full_path
val current_mp : unit -> Names.ModPath.t
Kernel-side names
val make_kn : Names.Id.t -> Names.KerName.t
type discharged_item =
| DischargedExport of Libobject.ExportObj.t |
| DischargedLeaf of Libobject.discharged_obj |
type classified_objects = {
substobjs : Libobject.t list; |
keepobjs : Libobject.t list; |
escapeobjs : Libobject.t list; |
anticipateobjs : Libobject.t list; |
}
module type StagedLibS = sig ... end
The StagedLibS
abstraction describes operations and traversal for Lib at a given stage.
We provide two instances of StagedLibS
, corresponding to the Synterp and Interp stages.
module Synterp : StagedLibS with type summary = Summary.Synterp.frozen
module Interp : StagedLibS with type summary = Summary.Interp.frozen
val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
type compilation_result = {
info : Library_info.t; |
synterp_objects : classified_objects; |
interp_objects : classified_objects; |
}
val end_compilation : Names.DirPath.t -> compilation_result
Finalize the compilation of a library.
val library_dp : unit -> Names.DirPath.t
The function library_dp
returns the DirPath.t
of the current compiling library (or default_library
)
val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
Extract the library part of a name even if in a section
val library_part : Names.GlobRef.t -> Names.DirPath.t
val section_segment_of_constant : Names.Constant.t -> Cooking.cooking_info
Section management for discharge
val section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info
val section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info
val section_instance : Names.GlobRef.t -> Constr.t array
val is_in_section : Names.GlobRef.t -> bool
val discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t
discharge_proj_repr p
discharges projection p
if the associated record was defined in the current section. If that is not the case, it returns p
unchanged.
Compatibility layer
Lib.StagedLibS
The StagedLibS
abstraction describes operations and traversal for Lib at a given stage.
type classified_objects = {
substobjs : Libobject.t list; |
keepobjs : Libobject.t list; |
anticipateobjs : Libobject.t list; |
}
val classify_segment : Libobject.t list -> classified_objects
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Lib.StagedLibS
The StagedLibS
abstraction describes operations and traversal for Lib at a given stage.
val find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node
Returns the opening node of a given name
val add_leaf_entry : Libobject.t -> unit
val open_section : Names.Id.t -> unit
Sections
val close_section : unit -> discharged_item list
close_section
needs to redo Export, so the complete implementation needs to involve Declaremods
.
val start_module : export -> Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> summary -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val declare_info : Library_info.t -> unit
Libobject
Libobject
declares persistent objects, given with methods:
* a caching function specifying how to add the object in the current scope; called when the object is added and after the end of the containing sections. If the object wishes to register its visibility in the Nametab, it should do so for all possible suffixes.
* a loading function, specifying what to do when the module containing the object is loaded; called at Require and after the end of the containing modules. If the object wishes to register its visibility in the Nametab, it should do so for all suffixes no shorter than the "int" argument
* an opening function, specifying what to do when the module containing the object is opened; called when the containing modules are Imported. Objects which should only have an effect when the nearest containing module is imported (and not when the modules containing the nearest module are imported) must check that the "int" argument is 1
. If the object wishes to register its visibility in the Nametab, it should do so for the suffix of the length the "int" argument
* a classification function, specifying what to do with the object, when the current module (containing the object) is ended; The possibilities are: Dispose - the object is dropped at the end of the module. Substitute - the object is kept at the end of the module. When the module is cloned (Include, module aliases) or when it's a module type which is getting instantiated (eg if module type T
is used for a functor argument X : T
or Declare Module X : T
), the substitution function is called on the object to update the module name. Keep - the object is kept at the end of the module. When the module is cloned the object is not cloned with it. This means that Keep objects in a module type or functor are dropped. Anticipate - this is for objects that have to be explicitly managed by the end_module
function (currently only Require).
* a substitution function, performing the substitution; this function should be declared for substitutive objects only (see above). NB: the substitution might be delayed instead of happening at module creation, so this function should _not_ depend on the current environment
* a discharge function, that is called at section closing time to collect the data necessary to rebuild the discharged form of the non volatile objects. If it returns None
the object is dropped. It is called in the state inside the section at its end, before it is reset. Notably the global environment contains the section data and the non-discharged globals.
* a rebuild function, that is applied after section closing to rebuild the non volatile content of a section from the data collected by the discharge function It is called in the state after the end of the section with any previous objects already present. Notably the global environment contains the discharged globals.
Any type defined as a persistent object must be pure (e.g. no references) and marshallable by the OCaml Marshal module (e.g. no closures).
Both names are passed to objects: a "semantic" kernel_name
, which can be substituted and a "syntactic" full_path
which can be printed
type object_name = Libnames.full_path * Names.KerName.t
type ('a, 'b, 'discharged) object_declaration = {
object_name : string; |
object_stage : Summary.Stage.t; |
cache_function : 'b -> unit; |
load_function : int -> 'b -> unit; |
open_function : open_filter -> int -> 'b -> unit; |
classify_function : 'a -> substitutivity; |
subst_function : (Mod_subst.substitution * 'a) -> 'a; |
discharge_function : 'a -> 'discharged option; |
rebuild_function : 'discharged -> 'a; |
}
val unfiltered : open_filter
val make_filter : finite:bool -> string CAst.t list -> open_filter
Anomaly when the list is empty.
val create_category : string -> category
Anomaly if called more than once for a given string.
val in_filter : cat:category option -> open_filter -> bool
On cat:None
, returns whether the filter allows opening uncategorized objects.
On cat:(Some category)
, returns whether the filter allows opening objects in the given category
.
val simple_open : ?cat:category -> ('i -> 'a -> unit) -> open_filter -> 'i -> 'a -> unit
Combinator for making objects with simple category-based open behaviour. When cat:None
, can be opened by Unfiltered, but also by Filtered with a negative set.
val filter_eq : open_filter -> open_filter -> bool
val filter_and : open_filter -> open_filter -> open_filter option
Returns None
when the intersection is empty.
val filter_or : open_filter -> open_filter -> open_filter
The default object is a "Keep" object with empty methods. Object creators are advised to use the construction * a caching function specifying how to add the object in the current scope; called when the object is added and after the end of the containing sections. If the object wishes to register its visibility in the Nametab, it should do so for all possible suffixes. * a loading function, specifying what to do when the module containing the object is loaded; called at Require and after the end of the containing modules. If the object wishes to register its visibility in the Nametab, it should do so for all suffixes no shorter than the "int" argument * an opening function, specifying what to do when the module containing the object is opened; called when the containing modules are Imported. Objects which should only have an effect when the nearest containing module is imported (and not when the modules containing the nearest module are imported) must check that the "int" argument is * a classification function, specifying what to do with the object, when the current module (containing the object) is ended; The possibilities are: Dispose - the object is dropped at the end of the module. Substitute - the object is kept at the end of the module. When the module is cloned (Include, module aliases) or when it's a module type which is getting instantiated (eg if module type * a substitution function, performing the substitution; this function should be declared for substitutive objects only (see above). NB: the substitution might be delayed instead of happening at module creation, so this function should _not_ depend on the current environment * a discharge function, that is called at section closing time to collect the data necessary to rebuild the discharged form of the non volatile objects. If it returns * a rebuild function, that is applied after section closing to rebuild the non volatile content of a section from the data collected by the discharge function It is called in the state after the end of the section with any previous objects already present. Notably the global environment contains the discharged globals. Any type defined as a persistent object must be pure (e.g. no references) and marshallable by the OCaml Marshal module (e.g. no closures). Both names are passed to objects: a "semantic" Anomaly when the list is empty. Anomaly if called more than once for a given string. On On Combinator for making objects with simple category-based open behaviour. When Returns The default object has empty methods. Object creators are advised to use the construction the identity substitution function Given an object declaration, the function Object declaration and names: if you need the current prefix (typically to interact with the nametab), you need to have it passed to you. The classify_function must be specified. the identity substitution function Given an object declaration, the function Object declaration and names: if you need the current prefix (typically to interact with the nametab), you need to have it passed to you. Object with semi-static scoping: the scoping depends on the given It is up to the caller of If Higher-level API for objects with fixed scope. We recommend to avoid declaring superglobal objects and using the nodischarge variants.{(default_object "MY_OBJECT") with
+
Module
Libobject
Libobject
declares persistent objects, given with methods:1
. If the object wishes to register its visibility in the Nametab, it should do so for the suffix of the length the "int" argumentT
is used for a functor argument X : T
or Declare Module X : T
), the substitution function is called on the object to update the module name. Keep - the object is kept at the end of the module. When the module is cloned the object is not cloned with it. This means that Keep objects in a module type or functor are dropped. Escape - like Keep, but also escapes module types, functors and opaque modules. Monomorphic universes and universe constraints behave like this. Anticipate - this is for objects that have to be explicitly managed by the end_module
function (currently only Require).None
the object is dropped. It is called in the state inside the section at its end, before it is reset. Notably the global environment contains the section data and the non-discharged globals.kernel_name
, which can be substituted and a "syntactic" full_path
which can be printedtype object_name = Libnames.full_path * Names.KerName.t
type ('a, 'b, 'discharged) object_declaration = {
object_name : string;
object_stage : Summary.Stage.t;
cache_function : 'b -> unit;
load_function : int -> 'b -> unit;
open_function : open_filter -> int -> 'b -> unit;
classify_function : 'a -> substitutivity;
subst_function : (Mod_subst.substitution * 'a) -> 'a;
discharge_function : 'a -> 'discharged option;
rebuild_function : 'discharged -> 'a;
}
val unfiltered : open_filter
val make_filter : finite:bool -> string CAst.t list -> open_filter
val create_category : string -> category
val in_filter : cat:category option -> open_filter -> bool
cat:None
, returns whether the filter allows opening uncategorized objects.cat:(Some category)
, returns whether the filter allows opening objects in the given category
.val simple_open : ?cat:category -> ('i -> 'a -> unit) -> open_filter -> 'i -> 'a -> unit
cat:None
, can be opened by Unfiltered, but also by Filtered with a negative set.val filter_eq : open_filter -> open_filter -> bool
val filter_and : open_filter -> open_filter -> open_filter option
None
when the intersection is empty.val filter_or : open_filter -> open_filter -> open_filter
{(default_object "MY_OBJECT") with
cache_function = ...
- }
and specify only these functions which are not empty/meaninglessval default_object : ?stage:Summary.Stage.t -> string -> ('a, 'b, 'a) object_declaration
val ident_subst_function : (Mod_subst.substitution * 'a) -> 'a
...
declare_object_full
will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects.type obj = Dyn.t
module ExportObj : sig ... end
and t =
| ModuleObject of Names.Id.t * substitutive_objects
| ModuleTypeObject of Names.Id.t * substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of Names.Id.t * t list
| ExportObject of ExportObj.t
| AtomicObject of obj
and substitutive_objects = Names.MBId.t list * algebraic_objects
declare_named_object_gen
passes the raw prefix which you can manipulate as you wish.declare_named_object_full
and declare_named_object
provide the convenience of packaging it with the provided Id.t
into a object_name
.declare_object
and declare_object_full
ignore the prefix for you.val declare_object : ('a, 'a, _) object_declaration -> 'a -> obj
val declare_object_full : ('a, 'a, _) object_declaration -> 'a Dyn.tag
val declare_named_object_full : ('a, object_name * 'a, _) object_declaration -> (Names.Id.t * 'a) Dyn.tag
val declare_named_object : ('a, object_name * 'a, _) object_declaration -> Names.Id.t -> 'a -> obj
val declare_named_object_gen : ('a, Nametab.object_prefix * 'a, _) object_declaration -> 'a -> obj
val cache_object : (Nametab.object_prefix * obj) -> unit
val load_object : int -> (Nametab.object_prefix * obj) -> unit
val open_object : open_filter -> int -> (Nametab.object_prefix * obj) -> unit
val subst_object : (Mod_subst.substitution * obj) -> obj
val classify_object : obj -> substitutivity
val object_stage : obj -> Summary.Stage.t
val discharge_object : obj -> discharged_obj option
val rebuild_object : discharged_obj -> obj
val object_with_locality : ?stage:Summary.Stage.t -> ?cat:category -> string -> cache:('a -> unit) ->
+ }
and specify only these functions which are not empty/meaninglessval default_object : ?stage:Summary.Stage.t -> string -> ('a, 'b, 'a) object_declaration
val ident_subst_function : (Mod_subst.substitution * 'a) -> 'a
...
declare_object_full
will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects.type obj = Dyn.t
module ExportObj : sig ... end
and t =
| ModuleObject of Names.Id.t * substitutive_objects
| ModuleTypeObject of Names.Id.t * substitutive_objects
| IncludeObject of algebraic_objects
| KeepObject of Names.Id.t * t list
| EscapeObject of Names.Id.t * t list
| ExportObject of ExportObj.t
| AtomicObject of obj
and substitutive_objects = Names.MBId.t list * algebraic_objects
declare_named_object_gen
passes the raw prefix which you can manipulate as you wish.declare_named_object_full
and declare_named_object
provide the convenience of packaging it with the provided Id.t
into a object_name
.declare_object
and declare_object_full
ignore the prefix for you.val declare_object : ('a, 'a, _) object_declaration -> 'a -> obj
val declare_object_full : ('a, 'a, _) object_declaration -> 'a Dyn.tag
val declare_named_object_full : ('a, object_name * 'a, _) object_declaration -> (Names.Id.t * 'a) Dyn.tag
val declare_named_object : ('a, object_name * 'a, _) object_declaration -> Names.Id.t -> 'a -> obj
val declare_named_object_gen : ('a, Nametab.object_prefix * 'a, _) object_declaration -> 'a -> obj
val cache_object : (Nametab.object_prefix * obj) -> unit
val load_object : int -> (Nametab.object_prefix * obj) -> unit
val open_object : open_filter -> int -> (Nametab.object_prefix * obj) -> unit
val subst_object : (Mod_subst.substitution * obj) -> obj
val classify_object : obj -> substitutivity
val object_stage : obj -> Summary.Stage.t
val discharge_object : obj -> discharged_obj option
val rebuild_object : discharged_obj -> obj
val object_with_locality : ?stage:Summary.Stage.t -> ?cat:category -> string -> cache:('a -> unit) ->
subst:((Mod_subst.substitution * 'a) -> 'a) option -> discharge:('a -> 'a) -> (locality * 'a, locality * 'a, locality * 'a) object_declaration
locality
not the rest of the object.add_leaf
to produce sensible errors if a value which cannot be discharged is given with non Local locality.subst
is None
non Local
values are Keep
, otherwise Substitute
.Export
values are only imported with shallow imports (depth = 1).cat
only matters when importing, ie only for Export
values.val local_object : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) ->
discharge:('a -> 'a option) -> ('a, 'a, 'a) object_declaration
val local_object_nodischarge : ?stage:Summary.Stage.t -> string -> cache:('a -> unit) ->
('a, 'a, 'a) object_declaration
val global_object : ?cat:category -> ?stage:Summary.Stage.t -> string -> cache:('a -> unit) ->
diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree
index 1df617c901..12da6e8521 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/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree
index 4d62c795ca..2c9ecdeda5 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/environment.pickle b/master/refman/.doctrees/environment.pickle
index 6a7454c694..d146f8fc2e 100644
Binary files a/master/refman/.doctrees/environment.pickle and b/master/refman/.doctrees/environment.pickle differ
diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree
index 9fe1292b42..06c6fd1263 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/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree
index 629fdf126a..9a41addcef 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/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree
index f59d69a4c0..9538a42304 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/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree
index 857a338c71..6152ad9b24 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 e2fea27417..17bc68c209 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 a68ec2f956..74313d8453 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 819b47c21c..5100cb3980 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/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree
index 5dbc552571..1e6f681ef0 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 c6319f98fb..843b3e0548 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 ff185239f9..eea89e445b 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 2fcef3b372..c8747137ca 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 281a7c4cc1..fe1bfdba9d 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/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree
index 3a28c0bef8..379f4a14d6 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 3cdb05c65a..3b52bb4fc1 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 1dff554f71..58f2074dcb 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 06ade9ef03..0609f30d24 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/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree
index b5c9ccc742..e8edbccf2b 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/language/extensions/match.html b/master/refman/language/extensions/match.html
index c3ece0056a..f488c5bf4e 100644
--- a/master/refman/language/extensions/match.html
+++ b/master/refman/language/extensions/match.html
@@ -1563,13 +1563,13 @@
Printing of hidden subtermsPrint
seq_rect.
Timing a tactic that evaluates to a term: time_constrpose v.
Profiling
L
Computing in a term: eval and EvalTime
assert (id (fact 8) = fact 8) by reflexivity.
-Computing in a term: eval and EvalTime
assert (id (fact 9) = fact 9) by reflexivity.
-Computing in a term: eval and EvalTime
assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity.
-match
construct","Setting properties of a function's arguments","Canonical Structures","Existential variables","Implicit arguments","Language extensions","Extended pattern matching","<no title>","<no title>","<no title>","<no title>","The Rocq Prover commands","CoqIDE","Building Rocq Projects","Ltac","Ltac2","<no title>","The SSReflect proof language","Tactics","Commands","Programmable proof search","Automatic solvers and programmable tactics","Solvers for logic and equality","Creating new tactics","Reasoning with equalities","Basic proof writing","Proof mode","Reasoning with inductive types","<no title>","Glossary index","<no title>","Syntax extensions and notation scopes","Functional induction","Libraries and plugins","Writing Rocq libraries and plugins","Documenting Rocq files with coqdoc","Command-line and graphical tools","Bibliography"],titleterms:{"0":[17,24],"0beta":17,"1":[17,24,37,67],"10":17,"11":17,"12":17,"13":17,"14":17,"15":17,"16":17,"17":17,"18":17,"19":17,"1beta":17,"1gamma":17,"2":[17,24,37,67],"20":17,"3":[17,24,71],"4":[17,24],"4beta":17,"4beta2":17,"5":[17,24],"5beta1":17,"5beta2":17,"5beta3":17,"5pl1":17,"5pl2":17,"5pl3":17,"6":[17,24],"6beta1":17,"7":[17,24],"8":17,"9":17,"\u03b1":31,"\u03b2":31,"\u03b4":31,"\u03b6":31,"\u03b7":31,"\u03b9":31,"abstract":[57,66],"boolean":[46,54,57],"byte":36,"case":[5,24,40,52,57,58,67],"catch":[54,55],"class":[3,4,37,55,71],"default":[41,46],"do":[11,54],"float":[27,36],"function":[4,28,30,34,41,44,54,60,72],"long":24,"new":[3,11,17,24,35,53,57,63],"short":5,"static":55,"switch":[55,57],"try":54,A:[2,14,35,58,67],In:55,Is:11,No:53,One:57,The:[11,26,27,34,35,44,51,53,57,71,75],_coqproject:53,abbrevi:[55,57,71],about:[7,46,71],access:37,ackermann:60,acknowledg:57,activ:4,ad:[3,11,52],addit:[2,57,60],advanc:[57,72],algorithm:64,alia:74,alias:46,altern:[41,54],alwai:64,ambigu:3,an:[35,57,59,67],analysi:67,annot:8,anonym:[37,57],antiquot:55,api:55,appendix:25,appli:[43,57,58,64,67],applic:[4,28,44,54,58],ar:[57,66],argument:[2,37,41,44,46,53,57,67,71],arithmet:[5,27],ariti:34,arrai:36,ask:9,assert:32,assert_fail:54,assert_succe:54,assign:57,associ:71,assumpt:[28,57],asynchron:[8,52],attribut:[4,17,18,29,35,38],autom:60,automat:[8,11,34,41,43,44,61,67],avail:4,avoid:2,axiom:2,b:58,backtrac:54,backtrack:[54,55,59],backward:[3,58],base:36,basic:[12,27,29,52,53,54,57,65,71],batch:51,beta1:17,beta2:17,beta3:17,beta:31,between:[2,55,59,66],bibliographi:77,bidirection:41,bind:[13,41,52,55,58,71],binder:[3,28,44,57,71],block:[8,57],bookkeep:57,both:71,bound:71,brace:66,branch:[54,57],breakpoint:52,buffer:52,build:[13,53],built:55,bullet:[57,66],calcul:66,calculu:26,call:[52,55],can:43,canon:42,cast:32,casual:44,caveat:[8,30],cell:55,chain:57,chang:[15,17,24,55],charact:52,check:54,checker:51,classic:58,claus:[37,46,58],clear:57,co:30,code:2,coercion:[4,46,71],cofix:30,coinduct:30,combin:[44,58,67],command:[3,13,17,19,24,35,51,52,57,59,66,67,71,75,76],comment:53,common:[53,58],compact:42,comparison:[54,55],compat:[10,17,37,55,57,74],compil:[17,51,52,53,59],complex:71,compon:55,compound:58,comput:[53,54,64],conclus:59,concret:[11,24],condit:[34,54,57],configur:53,conflict:2,confluenc:10,congruenc:57,connect:27,constant:[3,37,59,71],constraint:[14,66],construct:[12,24,26,34,37,40,54,59],constructor:[34,67],content:25,context:[3,13,54,55,57,58],contextu:[44,57],continu:[3,41,44],contradict:58,contravari:3,contribut:[2,24,27],control:[9,35,44,46,54,57,58,59,64,66],convent:[29,46],convers:[14,31,64],convert:31,coq:[24,27,52],coq_makefil:53,coqc:[51,53],coqchk:51,coqdep:53,coqdoc:75,coqid:[17,52],coqmakefil:53,coqrc:51,coqtop:51,core:33,corecurs:30,correct:34,count:54,covari:3,creat:[35,37,43,60,63],cumul:14,curli:66,custom:[51,52,71],cut:[5,54],cycl:66,databas:60,datatyp:27,deactiv:44,deal:11,debug:[12,54,55,59],debugg:[52,54],decid:[54,67],decis:5,declar:[3,13,38,41,42,44,55,57,66,67],defect:[54,57],defin:[10,34,35,37,54,55,60],definit:[3,9,12,14,30,32,34,37,40,46,54,55,57,64,71],delai:[55,66],delta:31,demonstr:14,depend:[17,46,53,58,59,67],deprec:[3,74],deriv:[6,42,67],descript:5,design:55,destruct:67,destructor:34,destructur:[46,57],detail:[2,17,24,53],detect:54,diff:66,differ:[2,44,66],disabl:71,disambigu:59,discharg:57,discrimin:67,discuss:11,disjunct:46,displai:[4,43,44,52,59,71],divis:2,document:[29,53,75],doe:[11,46],doesn:64,domain:7,dune:53,dynam:55,e:43,eappli:43,earli:24,eauto:13,edit:52,effect:[41,55],effici:24,elabor:9,element:[54,58],elim:57,elimin:[2,46,57],embed:53,emphasi:75,enabl:[3,66,71],encod:[12,52],end:[34,38],enter:66,entri:[57,71],environ:[51,59],equal:[7,9,27,62,64,67],equat:[11,57],equival:[57,58],error:[8,20,54,55],escap:75,essenti:29,eta:10,euclidean:2,eval:[54,64],evalu:[54,55],even:67,exact:57,exactly_onc:54,exampl:[2,3,4,5,6,11,14,17,26,27,28,29,30,31,34,35,37,38,40,41,42,43,44,46,51,52,53,54,55,57,58,59,60,62,64,66,67,71,72,74,75],except:55,execut:54,exist:[2,24,35],existenti:[43,57],exit:66,expans:[31,46],explicit:[14,43,44,57],explicitli:44,expos:59,express:[46,54,55,71],extend:[46,57],extens:[3,24,45,46,57,71],extra:[2,59],extract:[2,17,24],factor:[46,71],fail:[46,54,57],failur:54,famili:57,fast:[59,64],fatal:55,ffi:2,field:[11,35,37],file:[51,52,53,59,74,75],filenam:[2,53],fill:54,first:[3,34,46,54,57],fix:[31,34],fixpoint:[9,34],flag:[17,21,29,59],flow:[54,57,58],focus:[54,66],fold:64,fold_right:64,follow:44,foral:28,forbidden:53,forest:67,form:34,forward:58,found:27,frequent:9,fresh:54,from:[35,44,55],full:59,fun:28,function_scop:71,functor:35,gallina:57,gener:[2,3,4,11,14,23,29,44,54,55,57,67,71,72],get:[54,57],give:44,given:34,global:[14,54,71],glossari:69,goal:[5,11,54,55,57,58,66,67],grammar:[24,53],graph:4,graphic:76,guard:54,hand:46,have:[54,57],helper:67,hidden:46,hide:75,hierarchi:[13,42],high:5,higher:10,hint:[41,57,59,60],histor:24,histori:[11,15,24],hole:[10,54],horror:2,how:[11,66],html:75,hyperlink:75,hypothes:[54,55,58,59,66],hypothesi:[54,58],ident:[4,54],identifi:[59,71],idtac:54,implicit:[4,41,44,46,60,71],implicits_alt:41,impred:26,includ:58,incompat:[3,17],indent:57,index:[16,18,19,20,21,22,23,34,57,69],induct:[2,26,34,40,46,67,71,72],infer:[17,43,44],infix:71,inform:[66,71],infrastructur:17,inherit:[4,71],inlin:[2,59],innermost:3,input:52,insert:44,insid:[53,54,75],instal:53,instanc:[13,43],integ:[5,27,36,71],integr:7,interact:[8,35,44,51,54,55,57],interdepend:53,interfac:51,intern:59,interpret:[57,71],intro:[57,58],introduc:74,introduct:[3,25,57],intuitionist:54,invers:67,inversion_sigma:67,invoc:58,involv:[46,71],io:55,irrefut:46,irrelev:[12,31],is_cofix:54,is_fix:54,is_proj:54,isomorph:54,issu:[12,17,57],item:[35,57],iter:57,j:53,kei:52,kernel:17,keyword:[58,59],kind:44,knowledg:44,languag:[2,17,24,25,33,45,55,57],larger:67,late:53,latex:[53,75],launch:51,law:10,layer:55,lazy_match:55,lazymatch:54,least:54,left:67,leibniz:64,lemma:[9,27,66],let:[24,32,46,54,57],level:[5,10,29,30,32,34,55],lexic:29,lia:5,librari:[17,24,27,51,53,59,60,71,73,74],licit:57,limit:67,line:[17,51,75,76],linear:5,liner:57,list:[27,54,55,75],load:[51,53,59],local:[14,29,35,38,46,53,54,57,58,60,71],locat:[59,71],lock:57,logic:[27,53,54,60,62],loop:54,low:55,lower:34,lra:5,ltac1:55,ltac2:[17,55],ltac:[17,54,55],maccarthi:60,machin:59,macro:54,main:24,mainten:66,make:54,man:53,manag:[52,58,66],manipul:54,manual:[17,41,44],map:11,match:[31,34,37,40,46,54,55,57],materi:75,maxim:44,mechan:57,memori:66,meta:55,metavari:57,micromega:5,minim:14,miscellan:[17,24],ml:[2,55],mode:[8,44,52,55,57,66],modifi:53,modul:[4,35,53],monomorph:14,more:7,morphism:3,move:[57,58],multi:57,multi_match:55,multimatch:54,multipl:[37,41,46,53,54,55,57],museum:2,must:46,mutabl:55,mutual:34,n:67,name:[24,35,37,54,66],nat:[27,29],nativ:[17,53],native_comput:[53,64],natur:[54,55,60,67],neg:34,nest:[34,46],nia:5,non:[5,12,34,44,54,55,58,67,71],noncumul:14,nonreflex:3,nonsymmetr:3,notat:[17,27,42,54,55,59,71],notion:29,novelti:24,nra:5,nsatz:7,number:[27,54,60,71],numgoal:54,object:[34,36,46,74],oblig:9,ocaml:59,occurr:[34,57,58,67],odd:67,old:17,omit:35,onc:54,opam:53,opaqu:13,open:71,oper:59,optim:[2,54],option:[2,17,21,29,51,66,75],or_and_intropattern:67,order:[5,10,58],orient:58,other:[17,44,66],outermost:3,over:[5,9,55,57],overflow:29,overload:42,overview:[53,55],own:53,packag:53,page:53,parallel:8,paramet:[35,46,51,57],parameter:[13,34,71],parametr:[3,46,57],pars:[24,44,55,71],part:[59,75],partial:58,path:[53,59],pattern:[10,44,46,54,55,57,58,59,71],peano:27,perform:[53,58],permut:54,phrase:53,plane:5,plugin:[73,74],polymorph:[10,14,34,57],polynomi:11,posit:34,positivstellensatz:5,potenti:17,pre:5,preced:71,precompil:53,predefin:71,predic:[46,57,67],prefer:52,prelud:27,premis:[58,67],present:[4,14],preserv:10,pretti:[43,44,46,75],primit:[27,36,37,59,71],principl:[67,72,75],print:[3,4,14,37,43,44,46,54,55,59,71,75],privat:40,procedur:5,process:[5,8,54],produc:51,product:58,profil:[51,54,55],program:[2,6,9,27,55,60],programm:[60,61],progress:54,project:[37,53],proof:[5,8,12,14,25,31,32,46,54,57,58,60,65,66],prop:34,properti:[41,54,71],proposit:[12,27,54],prove:[54,66,67],prover:[25,51,53],provid:[3,46],psatz:5,qualifi:35,quantifi:27,queri:[52,59],question:9,quit:59,quot:53,quotat:55,radix:71,ration:[5,11],real:[5,17,27],realiz:2,reason:[58,64,67],recent:[15,17],record:[4,37],recurr:57,recurs:[27,30,34,55,71,72],redex:57,reduct:[24,31,34,37,55,59,64],refer:[17,54,59],reflect:57,refut:5,regist:59,registr:59,relat:3,remark:57,renam:41,reorder:[54,66],repeat:54,repetit:57,request:[59,66],reserv:[58,71],resili:8,resolut:[43,44,57],reus:37,revers:[4,44,54,55,64],revgoal:66,rewrit:[3,10,57,64,67],right:[46,67],ring:[5,11],rocq:[2,25,51,53,57,60,71,74,75],root:[24,53],rule:[10,26,31,34,38,57,64,71,75],run:[52,54],s:[2,27,41,67],same:[46,53],save:52,scheme:[67,72],scheme_typ:67,scope:[35,41,71],script:[51,52],search:[59,60],searchpattern:59,searchrewrit:59,second:[34,46,54,58],section:[4,13,14,38,66,75],select:57,selector:[54,57],semant:55,separ:66,sequenc:54,set:[2,13,26,29,37,41,57,58,60,66],setoid:[3,64],setup:53,share:35,shelv:66,shelve_unifi:66,shortcut:57,show:[66,75],side:[11,46],simpl:[28,31,34,35,55,64,71],simple_bind:58,simplif:57,simultan:71,singl:[51,54],soft:54,solv:[9,43,54,66],solver:[5,7,11,61,62],some:[2,27,35],sort:[14,34,39],sourc:[17,75],special:[57,58],specif:[17,25,27],specifi:14,split:[5,53],sprop:12,ssreflect:[17,57],stack:[29,52],standard:[17,24,27,55,57,60,71],start:[51,57],state:66,statu:59,step:[57,66],strategi:[3,46,64],strict:[12,34,44,55],strictli:34,string:[27,36,71],structur:[11,42,57],style:75,sub:35,subgoal:66,subpattern:46,subrel:3,subset:53,substitut:54,substructur:13,subterm:[43,46],subtyp:[26,44],succe:54,success:54,suff:57,suggest:8,summari:[13,17,24,35,38],superclass:13,support:[10,29,52],survei:27,swap:66,symbol:[10,52,54],synopsi:57,syntact:[9,54,55],syntax:[3,10,17,24,29,44,46,54,55,57,71],system:[2,35],t:64,tabl:[21,29],tactic:[3,5,11,17,22,24,27,43,54,55,57,58,60,61,63,64,67,71,72,74],target:[2,53],templat:[34,52],term:[26,54,55,64,71],termin:[10,12,57],test:[53,54],theorem:58,theori:34,thi:11,time:[51,53,54],time_constr:54,timeout:54,tool:[17,24,76],top:[30,32,34],toplevel:54,trace:54,trail:44,transit:55,transpar:13,tree:67,trigger:74,tryif:54,two:[35,54],type:[2,3,4,10,17,26,28,30,32,34,35,37,38,40,44,46,54,55,57,59,67,71],type_scop:71,type_term:54,typeclass:[13,57],uip:12,under:[3,57],understand:46,undo:64,unfold:[3,41,64],unicod:52,unif:[14,58,66],uninstal:53,univers:[10,14],unlock:57,unreleas:17,unset:29,until:58,untyp:54,unus:46,up:51,upgrad:53,us:[4,14,25,35,37,38,43,44,46,51,52,53,54,58,64,66,67,71],usag:[3,11,57,66,75],useless:2,user:[2,3,10,24,27],valu:[3,46,54,55],variabl:[11,43,44,46,51,52,55,66],varianc:14,variant:[40,46,57,58],variou:67,verbatim:75,version:[17,24,53],view:[5,57],vm_comput:64,vo:51,vocabulari:29,vs:[43,55,57],wai:[54,55],warn:[20,53,74],weak:14,well:[27,34],what:11,when:[44,46,57],wildcard:[46,57],wlog:57,work:[11,53,66],write:[46,65,74],your:53,zifi:5}})
\ No newline at end of file
+Search.setIndex({docnames:["addendum/canonical-structures","addendum/extended-pattern-matching","addendum/extraction","addendum/generalized-rewriting","addendum/implicit-coercions","addendum/micromega","addendum/miscellaneous-extensions","addendum/nsatz","addendum/parallel-proof-processing","addendum/program","addendum/rewrite-rules","addendum/ring","addendum/sprop","addendum/type-classes","addendum/universe-polymorphism","appendix/history-and-changes/index","appendix/indexes/index","changes","coq-attrindex","coq-cmdindex","coq-exnindex","coq-optindex","coq-tacindex","genindex","history","index","language/cic","language/coq-library","language/core/assumptions","language/core/basic","language/core/coinductive","language/core/conversion","language/core/definitions","language/core/index","language/core/inductive","language/core/modules","language/core/primitive","language/core/records","language/core/sections","language/core/sorts","language/core/variants","language/extensions/arguments-command","language/extensions/canonical","language/extensions/evars","language/extensions/implicit-arguments","language/extensions/index","language/extensions/match","language/gallina-extensions","language/gallina-specification-language","language/module-system","license","practical-tools/coq-commands","practical-tools/coqide","practical-tools/utilities","proof-engine/ltac","proof-engine/ltac2","proof-engine/proof-handling","proof-engine/ssreflect-proof-language","proof-engine/tactics","proof-engine/vernacular-commands","proofs/automatic-tactics/auto","proofs/automatic-tactics/index","proofs/automatic-tactics/logic","proofs/creating-tactics/index","proofs/writing-proofs/equality","proofs/writing-proofs/index","proofs/writing-proofs/proof-mode","proofs/writing-proofs/reasoning-inductives","proofs/writing-proofs/rewriting","std-glossindex","user-extensions/proof-schemes","user-extensions/syntax-extensions","using/libraries/funind","using/libraries/index","using/libraries/writing","using/tools/coqdoc","using/tools/index","zebibliography"],envversion:{"coqrst.coqdomain":2,"sphinx.domains.c":2,"sphinx.domains.changeset":1,"sphinx.domains.citation":1,"sphinx.domains.cpp":5,"sphinx.domains.index":1,"sphinx.domains.javascript":2,"sphinx.domains.math":2,"sphinx.domains.python":3,"sphinx.domains.rst":2,"sphinx.domains.std":2,"sphinx.ext.todo":2,sphinx:56},filenames:["addendum/canonical-structures.rst","addendum/extended-pattern-matching.rst","addendum/extraction.rst","addendum/generalized-rewriting.rst","addendum/implicit-coercions.rst","addendum/micromega.rst","addendum/miscellaneous-extensions.rst","addendum/nsatz.rst","addendum/parallel-proof-processing.rst","addendum/program.rst","addendum/rewrite-rules.rst","addendum/ring.rst","addendum/sprop.rst","addendum/type-classes.rst","addendum/universe-polymorphism.rst","appendix/history-and-changes/index.rst","appendix/indexes/index.rst","changes.rst","coq-attrindex.rst","coq-cmdindex.rst","coq-exnindex.rst","coq-optindex.rst","coq-tacindex.rst","genindex.rst","history.rst","index.rst","language/cic.rst","language/coq-library.rst","language/core/assumptions.rst","language/core/basic.rst","language/core/coinductive.rst","language/core/conversion.rst","language/core/definitions.rst","language/core/index.rst","language/core/inductive.rst","language/core/modules.rst","language/core/primitive.rst","language/core/records.rst","language/core/sections.rst","language/core/sorts.rst","language/core/variants.rst","language/extensions/arguments-command.rst","language/extensions/canonical.rst","language/extensions/evars.rst","language/extensions/implicit-arguments.rst","language/extensions/index.rst","language/extensions/match.rst","language/gallina-extensions.rst","language/gallina-specification-language.rst","language/module-system.rst","license.rst","practical-tools/coq-commands.rst","practical-tools/coqide.rst","practical-tools/utilities.rst","proof-engine/ltac.rst","proof-engine/ltac2.rst","proof-engine/proof-handling.rst","proof-engine/ssreflect-proof-language.rst","proof-engine/tactics.rst","proof-engine/vernacular-commands.rst","proofs/automatic-tactics/auto.rst","proofs/automatic-tactics/index.rst","proofs/automatic-tactics/logic.rst","proofs/creating-tactics/index.rst","proofs/writing-proofs/equality.rst","proofs/writing-proofs/index.rst","proofs/writing-proofs/proof-mode.rst","proofs/writing-proofs/reasoning-inductives.rst","proofs/writing-proofs/rewriting.rst","std-glossindex.rst","user-extensions/proof-schemes.rst","user-extensions/syntax-extensions.rst","using/libraries/funind.rst","using/libraries/index.rst","using/libraries/writing.rst","using/tools/coqdoc.rst","using/tools/index.rst","zebibliography.rst"],objects:{"":[[71,0,1,"coq:exn.'via'-and-'abstract'-cannot-be-used-together","'via' and 'abstract' cannot be used together"],[54,1,1,"coq:tacn.+-(backtracking-branching)","+ (backtracking branching)"],[57,1,1,"coq:tacn.=>","=>"],[66,3,1,"coq:cmd.Abort","Abort"],[59,3,1,"coq:cmd.About","About"],[71,2,1,"coq:warn.Activation-of-abbreviations-does-not-expect-mentioning-a-grammar-entry","Activation of abbreviations does not expect mentioning a grammar entry"],[71,2,1,"coq:warn.Activation-of-abbreviations-does-not-expect-mentioning-a-scope","Activation of abbreviations does not expect mentioning a scope"],[29,3,1,"coq:cmd.Add","Add"],[11,3,1,"coq:cmd.Add-Field","Add Field"],[3,3,1,"coq:cmd.Add-Morphism","Add Morphism"],[3,3,1,"coq:cmd.Add-Parametric-Morphism","Add Parametric Morphism"],[3,3,1,"coq:cmd.Add-Parametric-Relation","Add Parametric Relation"],[3,3,1,"coq:cmd.Add-Parametric-Setoid","Add Parametric Setoid"],[3,3,1,"coq:cmd.Add-Relation","Add Relation"],[11,3,1,"coq:cmd.Add-Ring","Add Ring"],[3,3,1,"coq:cmd.Add-Setoid","Add Setoid"],[5,3,1,"coq:cmd.Add-Zify","Add Zify"],[9,3,1,"coq:cmd.Admit-Obligations","Admit Obligations"],[66,3,1,"coq:cmd.Admitted","Admitted"],[12,4,1,"coq:flag.Allow-StrictProp","Allow StrictProp"],[44,0,1,"coq:exn.Argument-at-position-\u2018natural\u2019-is-mentioned-more-than-once","Argument at position \u2018natural\u2019 is mentioned more than once"],[54,0,1,"coq:exn.Argument-of-match-does-not-evaluate-to-a-term","Argument of match does not evaluate to a term"],[41,3,1,"coq:cmd.Arguments","Arguments"],[44,0,1,"coq:exn.Arguments-given-by-name-or-position-not-supported-in-explicit-mode","Arguments given by name or position not supported in explicit mode"],[11,0,1,"coq:exn.Arguments-of-ring_simplify-do-not-have-all-the-same-type","Arguments of ring_simplify do not have all the same type"],[41,0,1,"coq:exn.Arguments-of-section-variables-such-as-\u2018name\u2019-may-not-be-renamed","Arguments of section variables such as \u2018name\u2019 may not be renamed"],[46,4,1,"coq:flag.Asymmetric-Patterns","Asymmetric Patterns"],[66,0,1,"coq:exn.Attempt-to-save-an-incomplete-proof","Attempt to save an incomplete proof"],[29,3,1,"coq:cmd.Attributes","Attributes"],[34,4,1,"coq:flag.Auto-Template-Polymorphism","Auto Template Polymorphism"],[34,4,1,"coq:flag.Automatic-Proposition-Inductives","Automatic Proposition Inductives"],[34,2,1,"coq:warn.Automatically-declaring-\u2018ident\u2019-as-template-polymorphic","Automatically declaring \u2018ident\u2019 as template polymorphic"],[28,3,1,"coq:cmd.Axiom","Axiom"],[28,3,1,"coq:cmd.Axioms","Axioms"],[59,3,1,"coq:cmd.Back","Back"],[59,3,1,"coq:cmd.BackTo","BackTo"],[11,0,1,"coq:exn.Bad-lemma-for-decidability-of-equality","Bad lemma for decidability of equality"],[59,0,1,"coq:exn.Bad-magic-number","Bad magic number"],[64,0,1,"coq:exn.Bad-occurrence-number-of-\u2018qualid\u2019","Bad occurrence number of \u2018qualid\u2019"],[12,2,1,"coq:warn.Bad-relevance","Bad relevance"],[11,0,1,"coq:exn.Bad-ring-structure","Bad ring structure"],[71,3,1,"coq:cmd.Bind-Scope","Bind Scope"],[67,4,1,"coq:flag.Boolean-Equality-Schemes","Boolean Equality Schemes"],[5,5,1,"coq:thm.Bound-on-the-ceiling-function","Bound on the ceiling function"],[66,0,1,"coq:exn.Brackets-do-not-support-multi-goal-selectors","Brackets do not support multi-goal selectors"],[66,6,1,"coq:opt.Bullet-Behavior","Bullet Behavior"],[72,2,1,"coq:warn.Cannot-build-functional-inversion-principle","Cannot build functional inversion principle"],[58,0,1,"coq:exn.Cannot-change-\u2018ident\u2019,-it-is-used-in-conclusion","Cannot change \u2018ident\u2019, it is used in conclusion"],[58,0,1,"coq:exn.Cannot-change-\u2018ident\u2019,-it-is-used-in-hypothesis-\u2018ident\u2019","Cannot change \u2018ident\u2019, it is used in hypothesis \u2018ident\u2019"],[60,0,1,"coq:exn.Cannot-coerce-\u2018qualid\u2019-to-an-evaluable-reference","Cannot coerce \u2018qualid\u2019 to an evaluable reference"],[72,2,1,"coq:warn.Cannot-define-graph-for-\u2018ident\u2019","Cannot define graph for \u2018ident\u2019"],[72,2,1,"coq:warn.Cannot-define-principle(s)-for-\u2018ident\u2019","Cannot define principle(s) for \u2018ident\u2019"],[11,0,1,"coq:exn.Cannot-find-a-declared-ring-structure-for-equality-\u2018term\u2019","Cannot find a declared ring structure for equality \u2018term\u2019"],[11,0,1,"coq:exn.Cannot-find-a-declared-ring-structure-over-\u2018term\u2019","Cannot find a declared ring structure over \u2018term\u2019"],[64,0,1,"coq:exn.Cannot-find-a-relation-to-rewrite","Cannot find a relation to rewrite"],[64,0,1,"coq:exn.Cannot-find-any-non-recursive-equality-over-\u2018ident\u2019","Cannot find any non-recursive equality over \u2018ident\u2019"],[72,0,1,"coq:exn.Cannot-find-induction-information-on-\u2018qualid\u2019","Cannot find induction information on \u2018qualid\u2019"],[72,0,1,"coq:exn.Cannot-find-inversion-information-for-hypothesis-\u2018ident\u2019","Cannot find inversion information for hypothesis \u2018ident\u2019"],[59,0,1,"coq:exn.Cannot-find-library-foo-in-loadpath","Cannot find library foo in loadpath"],[4,0,1,"coq:exn.Cannot-find-the-source-class-of-\u2018qualid\u2019","Cannot find the source class of \u2018qualid\u2019"],[4,0,1,"coq:exn.Cannot-find-the-target-class","Cannot find the target class"],[35,2,1,"coq:warn.Cannot-import-local-constant,-it-will-be-ignored","Cannot import local constant, it will be ignored"],[71,0,1,"coq:exn.Cannot-interpret-in-\u2018scope_name\u2019-because-\u2018qualid\u2019-could-not-be-found-in-the-current-environment","Cannot interpret in \u2018scope_name\u2019 because \u2018qualid\u2019 could not be found in the current environment"],[71,0,1,"coq:exn.Cannot-interpret-this-number-as-a-value-of-type-\u2018type\u2019","Cannot interpret this number as a value of type \u2018type\u2019"],[71,0,1,"coq:exn.Cannot-interpret-this-string-as-a-value-of-type-\u2018type\u2019","Cannot interpret this string as a value of type \u2018type\u2019"],[59,0,1,"coq:exn.Cannot-load-\u2018qualid\u2019:-no-physical-path-bound-to-\u2018dirpath\u2019","Cannot load \u2018qualid\u2019: no physical path bound to \u2018dirpath\u2019"],[58,0,1,"coq:exn.Cannot-move-\u2018ident\u2019-after-\u2018ident\u2019:-it-depends-on-\u2018ident\u2019","Cannot move \u2018ident\u2019 after \u2018ident\u2019: it depends on \u2018ident\u2019"],[58,0,1,"coq:exn.Cannot-move-\u2018ident\u2019-after-\u2018ident\u2019:-it-occurs-in-the-type-of-\u2018ident\u2019","Cannot move \u2018ident\u2019 after \u2018ident\u2019: it occurs in the type of \u2018ident\u2019"],[62,0,1,"coq:exn.Cannot-recognize-a-boolean-equality","Cannot recognize a boolean equality"],[67,0,1,"coq:exn.Cannot-recognize-a-statement-based-on-\u2018reference\u2019","Cannot recognize a statement based on \u2018reference\u2019"],[4,0,1,"coq:exn.Cannot-recognize-\u2018coercion_class\u2019-as-a-source-class-of-\u2018qualid\u2019","Cannot recognize \u2018coercion_class\u2019 as a source class of \u2018qualid\u2019"],[64,0,1,"coq:exn.Cannot-turn-[inductive|constructor]-into-an-evaluable-reference","Cannot turn [inductive|constructor] into an evaluable reference"],[72,0,1,"coq:exn.Cannot-use-mutual-definition-with-well-founded-recursion-or-measure","Cannot use mutual definition with well-founded recursion or measure"],[42,3,1,"coq:cmd.Canonical-Structure","Canonical Structure"],[59,0,1,"coq:exn.Can\u2019t-find-file-\u2018ident\u2019-on-loadpath","Can\u2019t find file \u2018ident\u2019 on loadpath"],[67,4,1,"coq:flag.Case-Analysis-Schemes","Case Analysis Schemes"],[5,5,1,"coq:thm.Case-split","Case split"],[40,0,1,"coq:exn.Casts-are-not-supported-in-this-pattern","Casts are not supported in this pattern"],[2,3,1,"coq:cmd.Cd","Cd"],[59,3,1,"coq:cmd.Check","Check"],[13,3,1,"coq:cmd.Class","Class"],[71,3,1,"coq:cmd.Close-Scope","Close Scope"],[30,3,1,"coq:cmd.CoFixpoint","CoFixpoint"],[30,3,1,"coq:cmd.CoInductive","CoInductive"],[4,3,1,"coq:cmd.Coercion","Coercion"],[66,3,1,"coq:cmd.Collection","Collection"],[67,3,1,"coq:cmd.Combined-Scheme","Combined Scheme"],[29,3,1,"coq:cmd.Comments","Comments"],[64,3,1,"coq:cmd.Compute","Compute"],[54,0,1,"coq:exn.Condition-not-satisfied","Condition not satisfied"],[28,3,1,"coq:cmd.Conjecture","Conjecture"],[28,3,1,"coq:cmd.Conjectures","Conjectures"],[14,3,1,"coq:cmd.Constraint","Constraint"],[38,3,1,"coq:cmd.Context","Context"],[44,4,1,"coq:flag.Contextual-Implicit","Contextual Implicit"],[51,4,1,"coq:flag.Coqtop-Exit-On-Error","Coqtop Exit On Error"],[32,3,1,"coq:cmd.Corollary","Corollary"],[60,3,1,"coq:cmd.Create-HintDb","Create HintDb"],[14,7,1,"coq:attr.Cumulative","Cumulative"],[14,4,1,"coq:flag.Cumulativity-Weak-Constraints","Cumulativity Weak Constraints"],[54,3,1,"coq:cmd.Debug","Debug"],[59,6,1,"coq:opt.Debug","Debug"],[60,4,1,"coq:flag.Debug-Auto","Debug Auto"],[60,4,1,"coq:flag.Debug-Eauto","Debug Eauto"],[57,4,1,"coq:flag.Debug-SsrMatching","Debug SsrMatching"],[57,4,1,"coq:flag.Debug-Ssreflect","Debug Ssreflect"],[60,4,1,"coq:flag.Debug-Trivial","Debug Trivial"],[54,0,1,"coq:exn.Debug-mode-not-available-in-the-IDE","Debug mode not available in the IDE"],[67,4,1,"coq:flag.Decidable-Equality-Schemes","Decidable Equality Schemes"],[71,3,1,"coq:cmd.Declare-Custom-Entry","Declare Custom Entry"],[64,3,1,"coq:cmd.Declare-Equivalent-Keys","Declare Equivalent Keys"],[13,3,1,"coq:cmd.Declare-Instance","Declare Instance"],[64,3,1,"coq:cmd.Declare-Left-Step","Declare Left Step"],[59,3,1,"coq:cmd.Declare-ML-Module","Declare ML Module"],[35,3,1,"coq:cmd.Declare-Module","Declare Module"],[3,3,1,"coq:cmd.Declare-Morphism","Declare Morphism"],[64,3,1,"coq:cmd.Declare-Reduction","Declare Reduction"],[64,3,1,"coq:cmd.Declare-Right-Step","Declare Right Step"],[71,3,1,"coq:cmd.Declare-Scope","Declare Scope"],[60,2,1,"coq:warn.Declaring-arbitrary-terms-as-hints-is-fragile-and-deprecated;-it-is-recommended-to-declare-a-toplevel-constant-instead","Declaring arbitrary terms as hints is fragile and deprecated; it is recommended to declare a toplevel constant instead"],[58,6,1,"coq:opt.Default-Goal-Selector","Default Goal Selector"],[66,6,1,"coq:opt.Default-Proof-Mode","Default Proof Mode"],[66,6,1,"coq:opt.Default-Proof-Using","Default Proof Using"],[59,6,1,"coq:opt.Default-Timeout","Default Timeout"],[66,3,1,"coq:cmd.Defined","Defined"],[32,3,1,"coq:cmd.Definition","Definition"],[12,4,1,"coq:flag.Definitional-UIP","Definitional UIP"],[71,3,1,"coq:cmd.Delimit-Scope","Delimit Scope"],[34,4,1,"coq:flag.Dependent-Proposition-Eliminators","Dependent Proposition Eliminators"],[6,3,1,"coq:cmd.Derive","Derive"],[67,3,1,"coq:cmd.Derive-Dependent-Inversion","Derive Dependent Inversion"],[67,3,1,"coq:cmd.Derive-Dependent-Inversion_clear","Derive Dependent Inversion_clear"],[67,3,1,"coq:cmd.Derive-Inversion","Derive Inversion"],[67,3,1,"coq:cmd.Derive-Inversion_clear","Derive Inversion_clear"],[66,6,1,"coq:opt.Diffs","Diffs"],[71,3,1,"coq:cmd.Disable-Notation","Disable Notation"],[59,3,1,"coq:cmd.Drop","Drop"],[5,6,1,"coq:opt.Dump-Arith","Dump Arith"],[59,0,1,"coq:exn.Dynlink-error:-execution-of-module-initializers-in-the","Dynlink error: execution of module initializers in the"],[46,0,1,"coq:exn.Either-there-is-a-type-incompatibility-or-the-problem-involves-dependencies","Either there is a type incompatibility or the problem involves dependencies"],[67,4,1,"coq:flag.Elimination-Schemes","Elimination Schemes"],[71,3,1,"coq:cmd.Enable-Notation","Enable Notation"],[38,3,1,"coq:cmd.End","End"],[71,0,1,"coq:exn.End-of-quoted-string-not-followed-by-a-space-in-notation","End of quoted string not followed by a space in notation"],[64,3,1,"coq:cmd.Eval","Eval"],[32,3,1,"coq:cmd.Example","Example"],[13,3,1,"coq:cmd.Existing-Class","Existing Class"],[13,3,1,"coq:cmd.Existing-Instance","Existing Instance"],[13,3,1,"coq:cmd.Existing-Instances","Existing Instances"],[35,3,1,"coq:cmd.Export","Export"],[54,0,1,"coq:exn.Expression-does-not-evaluate-to-a-tactic","Expression does not evaluate to a tactic"],[2,3,1,"coq:cmd.Extract-Callback","Extract Callback"],[2,0,1,"coq:exn.Extract-Callback-is-supported-only-for-OCaml-extraction","Extract Callback is supported only for OCaml extraction"],[2,3,1,"coq:cmd.Extract-Constant","Extract Constant"],[2,3,1,"coq:cmd.Extract-Foreign-Constant","Extract Foreign Constant"],[2,0,1,"coq:exn.Extract-Foreign-Constant-is-supported-only-for-OCaml-extraction","Extract Foreign Constant is supported only for OCaml extraction"],[2,0,1,"coq:exn.Extract-Foreign-Constant-is-supported-only-for-functions","Extract Foreign Constant is supported only for functions"],[2,3,1,"coq:cmd.Extract-Inductive","Extract Inductive"],[2,3,1,"coq:cmd.Extract-Inlined-Constant","Extract Inlined Constant"],[2,3,1,"coq:cmd.Extraction","Extraction"],[2,4,1,"coq:flag.Extraction-AutoInline","Extraction AutoInline"],[2,3,1,"coq:cmd.Extraction-Blacklist","Extraction Blacklist"],[2,4,1,"coq:flag.Extraction-Conservative-Types","Extraction Conservative Types"],[2,6,1,"coq:opt.Extraction-File-Comment","Extraction File Comment"],[2,6,1,"coq:opt.Extraction-Flag","Extraction Flag"],[2,3,1,"coq:cmd.Extraction-Implicit","Extraction Implicit"],[2,3,1,"coq:cmd.Extraction-Inline","Extraction Inline"],[2,4,1,"coq:flag.Extraction-KeepSingleton","Extraction KeepSingleton"],[2,3,1,"coq:cmd.Extraction-Language","Extraction Language"],[2,3,1,"coq:cmd.Extraction-Library","Extraction Library"],[2,3,1,"coq:cmd.Extraction-NoInline","Extraction NoInline"],[2,4,1,"coq:flag.Extraction-Optimize","Extraction Optimize"],[2,6,1,"coq:opt.Extraction-Output-Directory","Extraction Output Directory"],[2,4,1,"coq:flag.Extraction-SafeImplicits","Extraction SafeImplicits"],[2,3,1,"coq:cmd.Extraction-TestCompile","Extraction TestCompile"],[2,4,1,"coq:flag.Extraction-TypeExpand","Extraction TypeExpand"],[32,3,1,"coq:cmd.Fact","Fact"],[59,3,1,"coq:cmd.Fail","Fail"],[54,0,1,"coq:exn.Failed-to-progress","Failed to progress"],[59,4,1,"coq:flag.Fast-Name-Printing","Fast Name Printing"],[59,0,1,"coq:exn.File-not-found-on-loadpath:-\u2018string\u2019","File not found on loadpath: \u2018string\u2019"],[59,0,1,"coq:exn.Files-processed-by-Load-cannot-leave-open-proofs","Files processed by Load cannot leave open proofs"],[9,3,1,"coq:cmd.Final-Obligation","Final Obligation"],[62,6,1,"coq:opt.Firstorder-Depth","Firstorder Depth"],[62,6,1,"coq:opt.Firstorder-Solver","Firstorder Solver"],[34,3,1,"coq:cmd.Fixpoint","Fixpoint"],[41,0,1,"coq:exn.Flag-'rename'-expected-to-rename-\u2018name\u2019-into-\u2018name\u2019","Flag 'rename' expected to rename \u2018name\u2019 into \u2018name\u2019"],[66,3,1,"coq:cmd.Focus","Focus"],[46,0,1,"coq:exn.Found-a-constructor-of-inductive-type-term-while-a-constructor-of-term-is-expected","Found a constructor of inductive type term while a constructor of term is expected"],[64,0,1,"coq:exn.Found-an-\"at\"-clause-without-\"with\"-clause","Found an "at" clause without "with" clause"],[71,2,1,"coq:warn.Found-no-matching-notation-to-enable-or-disable","Found no matching notation to enable or disable"],[64,0,1,"coq:exn.Found-no-subterm-matching-\u2018term\u2019-in-the-current-goal","Found no subterm matching \u2018term\u2019 in the current goal"],[64,0,1,"coq:exn.Found-no-subterm-matching-\u2018term\u2019-in-\u2018ident\u2019","Found no subterm matching \u2018term\u2019 in \u2018ident\u2019"],[4,0,1,"coq:exn.Found-target-class-\u2018coercion_class\u2019-instead-of-\u2018coercion_class\u2019","Found target class \u2018coercion_class\u2019 instead of \u2018coercion_class\u2019"],[59,3,1,"coq:cmd.From-\u2026-Dependency","From \u2026 Dependency"],[59,3,1,"coq:cmd.From-\u2026-Require","From \u2026 Require"],[4,0,1,"coq:exn.Funclass-cannot-be-a-source-class","Funclass cannot be a source class"],[72,3,1,"coq:cmd.Function","Function"],[72,3,1,"coq:cmd.Functional-Case","Functional Case"],[72,3,1,"coq:cmd.Functional-Scheme","Functional Scheme"],[44,3,1,"coq:cmd.Generalizable","Generalizable"],[72,3,1,"coq:cmd.Generate-graph-for","Generate graph for"],[66,3,1,"coq:cmd.Goal","Goal"],[59,4,1,"coq:flag.Guard-Checking","Guard Checking"],[66,3,1,"coq:cmd.Guarded","Guarded"],[60,3,1,"coq:cmd.Hint-Constants","Hint Constants"],[60,3,1,"coq:cmd.Hint-Constructors","Hint Constructors"],[60,3,1,"coq:cmd.Hint-Cut","Hint Cut"],[60,3,1,"coq:cmd.Hint-Extern","Hint Extern"],[60,3,1,"coq:cmd.Hint-Immediate","Hint Immediate"],[60,3,1,"coq:cmd.Hint-Mode","Hint Mode"],[60,3,1,"coq:cmd.Hint-Opaque","Hint Opaque"],[60,3,1,"coq:cmd.Hint-Projections","Hint Projections"],[60,3,1,"coq:cmd.Hint-Resolve","Hint Resolve"],[60,3,1,"coq:cmd.Hint-Rewrite","Hint Rewrite"],[60,3,1,"coq:cmd.Hint-Transparent","Hint Transparent"],[60,3,1,"coq:cmd.Hint-Unfold","Hint Unfold"],[60,3,1,"coq:cmd.Hint-Variables","Hint Variables"],[57,3,1,"coq:cmd.Hint-View-for","Hint View for"],[57,3,1,"coq:cmd.Hint-View-for-apply","Hint View for apply"],[57,3,1,"coq:cmd.Hint-View-for-move","Hint View for move"],[28,3,1,"coq:cmd.Hypotheses","Hypotheses"],[28,3,1,"coq:cmd.Hypothesis","Hypothesis"],[72,0,1,"coq:exn.Hypothesis-\u2018ident\u2019-must-contain-at-least-one-Function","Hypothesis \u2018ident\u2019 must contain at least one Function"],[66,6,1,"coq:opt.Hyps-Limit","Hyps Limit"],[62,0,1,"coq:exn.I-don\u2019t-know-how-to-handle-dependent-equality","I don\u2019t know how to handle dependent equality"],[4,3,1,"coq:cmd.Identity-Coercion","Identity Coercion"],[13,2,1,"coq:warn.Ignored-instance-declaration-for-\u201c\u2018ident\u2019\u201d:-\u201c\u2018term\u2019\u201d-is-not-a-class","Ignored instance declaration for \u201c\u2018ident\u2019\u201d: \u201c\u2018term\u2019\u201d is not a class"],[44,2,1,"coq:warn.Ignoring-implicit-binder-declaration-in-unexpected-position","Ignoring implicit binder declaration in unexpected position"],[9,0,1,"coq:exn.Ill-formed-recursive-definition","Ill-formed recursive definition"],[34,0,1,"coq:exn.Ill-formed-template-inductive-declaration:-not-polymorphic-on-any-universe","Ill-formed template inductive declaration: not polymorphic on any universe"],[44,4,1,"coq:flag.Implicit-Arguments","Implicit Arguments"],[44,3,1,"coq:cmd.Implicit-Type","Implicit Type"],[44,3,1,"coq:cmd.Implicit-Types","Implicit Types"],[35,3,1,"coq:cmd.Import","Import"],[35,3,1,"coq:cmd.Include","Include"],[35,3,1,"coq:cmd.Include-Type","Include Type"],[57,0,1,"coq:exn.Incorrect-number-of-tactics-(expected-N-tactics,-was-given-M)","Incorrect number of tactics (expected N tactics, was given M)"],[34,3,1,"coq:cmd.Inductive","Inductive"],[71,3,1,"coq:cmd.Infix","Infix"],[54,3,1,"coq:cmd.Info","Info"],[60,4,1,"coq:flag.Info-Auto","Info Auto"],[60,4,1,"coq:flag.Info-Eauto","Info Eauto"],[54,6,1,"coq:opt.Info-Level","Info Level"],[5,4,1,"coq:flag.Info-Micromega","Info Micromega"],[60,4,1,"coq:flag.Info-Trivial","Info Trivial"],[59,3,1,"coq:cmd.Inspect","Inspect"],[13,3,1,"coq:cmd.Instance","Instance"],[59,3,1,"coq:cmd.Instructions","Instructions"],[62,4,1,"coq:flag.Intuition-Negation-Unfolding","Intuition Negation Unfolding"],[59,0,1,"coq:exn.Invalid-backtrack","Invalid backtrack"],[67,8,1,"coq:table.Keep-Equalities","Keep Equalities"],[67,4,1,"coq:flag.Keep-Proof-Equalities","Keep Proof Equalities"],[64,4,1,"coq:flag.Kernel-Term-Sharing","Kernel Term Sharing"],[64,4,1,"coq:flag.Keyed-Unification","Keyed Unification"],[38,0,1,"coq:exn.Last-block-to-end-has-name-\u2018ident\u2019","Last block to end has name \u2018ident\u2019"],[32,3,1,"coq:cmd.Lemma","Lemma"],[38,3,1,"coq:cmd.Let","Let"],[38,3,1,"coq:cmd.Let-CoFixpoint","Let CoFixpoint"],[38,3,1,"coq:cmd.Let-Fixpoint","Let Fixpoint"],[5,4,1,"coq:flag.Lia-Cache","Lia Cache"],[59,3,1,"coq:cmd.Load","Load"],[59,0,1,"coq:exn.Load-is-not-supported-inside-proofs","Load is not supported inside proofs"],[59,3,1,"coq:cmd.Locate","Locate"],[59,3,1,"coq:cmd.Locate-File","Locate File"],[59,3,1,"coq:cmd.Locate-Library","Locate Library"],[59,3,1,"coq:cmd.Locate-Ltac","Locate Ltac"],[59,3,1,"coq:cmd.Locate-Ltac2","Locate Ltac2"],[59,3,1,"coq:cmd.Locate-Module","Locate Module"],[59,3,1,"coq:cmd.Locate-Term","Locate Term"],[60,6,1,"coq:opt.Loose-Hint-Behavior","Loose Hint Behavior"],[54,3,1,"coq:cmd.Ltac","Ltac"],[54,4,1,"coq:flag.Ltac-Backtrace","Ltac Backtrace"],[54,4,1,"coq:flag.Ltac-Batch-Debug","Ltac Batch Debug"],[54,4,1,"coq:flag.Ltac-Debug","Ltac Debug"],[54,4,1,"coq:flag.Ltac-Profiling","Ltac Profiling"],[55,3,1,"coq:cmd.Ltac2","Ltac2"],[55,4,1,"coq:flag.Ltac2-Backtrace","Ltac2 Backtrace"],[55,3,1,"coq:cmd.Ltac2-Check","Ltac2 Check"],[55,3,1,"coq:cmd.Ltac2-Eval","Ltac2 Eval"],[55,3,1,"coq:cmd.Ltac2-Globalize","Ltac2 Globalize"],[55,4,1,"coq:flag.Ltac2-In-Ltac1-Profiling","Ltac2 In Ltac1 Profiling"],[55,3,1,"coq:cmd.Ltac2-Notation","Ltac2 Notation"],[55,3,1,"coq:cmd.Ltac2-Notation-(abbreviation)","Ltac2 Notation (abbreviation)"],[55,3,1,"coq:cmd.Ltac2-Set","Ltac2 Set"],[55,3,1,"coq:cmd.Ltac2-Type","Ltac2 Type"],[55,4,1,"coq:flag.Ltac2-Typed-Notations","Ltac2 Typed Notations"],[55,3,1,"coq:cmd.Ltac2-external","Ltac2 external"],[44,2,1,"coq:warn.Making-shadowed-name-of-implicit-argument-accessible-by-position","Making shadowed name of implicit argument accessible by position"],[66,4,1,"coq:flag.Mangle-Names","Mangle Names"],[66,4,1,"coq:flag.Mangle-Names-Light","Mangle Names Light"],[66,6,1,"coq:opt.Mangle-Names-Prefix","Mangle Names Prefix"],[44,4,1,"coq:flag.Maximal-Implicit-Insertion","Maximal Implicit Insertion"],[71,0,1,"coq:exn.Missing-mapping-for-constructor-\u2018qualid\u2019","Missing mapping for constructor \u2018qualid\u2019"],[35,3,1,"coq:cmd.Module","Module"],[35,3,1,"coq:cmd.Module-Type","Module Type"],[59,0,1,"coq:exn.Module/section-\u2018qualid\u2019-not-found","Module/section \u2018qualid\u2019 not found"],[14,7,1,"coq:attr.Monomorphic","Monomorphic"],[71,0,1,"coq:exn.More-than-one-interpretation-bound-to-this-notation,-confirm-with-the-\"all\"-modifier","More than one interpretation bound to this notation, confirm with the "all" modifier"],[71,0,1,"coq:exn.Multiple-'via'-options","Multiple 'via' options"],[71,0,1,"coq:exn.Multiple-'warning-after'-or-'abstract-after'-options","Multiple 'warning after' or 'abstract after' options"],[64,6,1,"coq:opt.NativeCompute-Profile-Filename","NativeCompute Profile Filename"],[64,4,1,"coq:flag.NativeCompute-Profiling","NativeCompute Profiling"],[64,4,1,"coq:flag.NativeCompute-Timing","NativeCompute Timing"],[66,4,1,"coq:flag.Nested-Proofs-Allowed","Nested Proofs Allowed"],[66,2,1,"coq:warn.New-Collection-definition-of-\u2018ident\u2019-shadows-the-previous-one","New Collection definition of \u2018ident\u2019 shadows the previous one"],[9,3,1,"coq:cmd.Next-Obligation","Next Obligation"],[5,4,1,"coq:flag.Nia-Cache","Nia Cache"],[54,0,1,"coq:exn.No-applicable-tactic","No applicable tactic"],[72,0,1,"coq:exn.No-argument-name-\u2018ident\u2019","No argument name \u2018ident\u2019"],[54,0,1,"coq:exn.No-evars","No evars"],[35,0,1,"coq:exn.No-field-named-\u2018ident\u2019-in-\u2018qualid\u2019","No field named \u2018ident\u2019 in \u2018qualid\u2019"],[66,0,1,"coq:exn.No-focused-proof","No focused proof"],[66,0,1,"coq:exn.No-focused-proof-(No-proof-editing-in-progress)","No focused proof (No proof-editing in progress)"],[66,0,1,"coq:exn.No-focused-proof-to-restart","No focused proof to restart"],[64,0,1,"coq:exn.No-head-constant-to-reduce","No head constant to reduce"],[54,0,1,"coq:exn.No-matching-clauses-for-match","No matching clauses for match"],[54,0,1,"coq:exn.No-matching-clauses-for-match-goal","No matching clauses for match goal"],[71,0,1,"coq:exn.No-notation-provided","No notation provided"],[67,0,1,"coq:exn.No-primitive-equality-found","No primitive equality found"],[58,0,1,"coq:exn.No-product-even-after-head-reduction","No product even after head-reduction"],[3,0,1,"coq:exn.No-progress-made","No progress made"],[58,0,1,"coq:exn.No-quantified-hypothesis-named-\u2018ident\u2019-in-current-goal-even-after-head-reduction","No quantified hypothesis named \u2018ident\u2019 in current goal even after head-reduction"],[58,0,1,"coq:exn.No-such-assumption","No such assumption"],[58,0,1,"coq:exn.No-such-binder","No such binder"],[58,0,1,"coq:exn.No-such-bound-variable-\u2018ident\u2019-(no-bound-variables-at-all-in-the-expression)","No such bound variable \u2018ident\u2019 (no bound variables at all in the expression)"],[66,0,1,"coq:exn.No-such-goal","No such goal"],[66,0,1,"coq:exn.No-such-goal-(\u2018ident\u2019)","No such goal (\u2018ident\u2019)"],[66,0,1,"coq:exn.No-such-goal-(\u2018natural\u2019)","No such goal (\u2018natural\u2019)"],[58,0,1,"coq:exn.No-such-hypothesis:-\u2018ident\u2019","No such hypothesis: \u2018ident\u2019"],[58,0,1,"coq:exn.No-\u2018natural\u2019-th-non-dependent-hypothesis-in-current-goal-even-after-head-reduction","No \u2018natural\u2019-th non dependent hypothesis in current goal even after head-reduction"],[46,0,1,"coq:exn.Non-exhaustive-pattern-matching","Non exhaustive pattern matching"],[9,0,1,"coq:exn.Non-extensible-universe-declaration-not-supported-with-monomorphic-Program-Definition","Non extensible universe declaration not supported with monomorphic Program Definition"],[34,0,1,"coq:exn.Non-strictly-positive-occurrence-of-\u2018ident\u2019-in-\u2018type\u2019","Non strictly positive occurrence of \u2018ident\u2019 in \u2018type\u2019"],[14,7,1,"coq:attr.NonCumulative","NonCumulative"],[67,4,1,"coq:flag.Nonrecursive-Elimination-Schemes","Nonrecursive Elimination Schemes"],[54,0,1,"coq:exn.Not-a-context-variable","Not a context variable"],[67,0,1,"coq:exn.Not-a-discriminable-equality","Not a discriminable equality"],[67,0,1,"coq:exn.Not-a-negated-primitive-equality","Not a negated primitive equality"],[11,0,1,"coq:exn.Not-a-valid-ring-equation","Not a valid ring equation"],[54,0,1,"coq:exn.Not-a-variable-or-hypothesis","Not a variable or hypothesis"],[54,0,1,"coq:exn.Not-an-evar","Not an evar"],[58,0,1,"coq:exn.Not-an-exact-proof","Not an exact proof"],[67,0,1,"coq:exn.Not-an-inductive-goal-with-1-constructor","Not an inductive goal with 1 constructor"],[67,0,1,"coq:exn.Not-an-inductive-goal-with-2-constructors","Not an inductive goal with 2 constructors"],[67,0,1,"coq:exn.Not-an-inductive-product","Not an inductive product"],[64,0,1,"coq:exn.Not-convertible","Not convertible"],[67,0,1,"coq:exn.Not-enough-constructors","Not enough constructors"],[44,0,1,"coq:exn.Not-enough-non-implicit-arguments-to-accept-the-argument-bound-to-\u2018ident\u2019","Not enough non implicit arguments to accept the argument bound to \u2018ident\u2019"],[44,0,1,"coq:exn.Not-enough-non-implicit-arguments-to-accept-the-argument-bound-to-\u2018natural\u2019","Not enough non implicit arguments to accept the argument bound to \u2018natural\u2019"],[54,0,1,"coq:exn.Not-equal","Not equal"],[54,0,1,"coq:exn.Not-equal-(due-to-universes)","Not equal (due to universes)"],[54,0,1,"coq:exn.Not-ground","Not ground"],[72,0,1,"coq:exn.Not-the-right-number-of-induction-arguments","Not the right number of induction arguments"],[58,0,1,"coq:exn.Not-the-right-number-of-missing-arguments-(expected-\u2018natural\u2019)","Not the right number of missing arguments (expected \u2018natural\u2019)"],[71,3,1,"coq:cmd.Notation","Notation"],[71,3,1,"coq:cmd.Notation-(abbreviation)","Notation (abbreviation)"],[55,0,1,"coq:exn.Notation-levels-must-range-between-0-and-6","Notation levels must range between 0 and 6"],[67,0,1,"coq:exn.Nothing-to-inject","Nothing to inject"],[3,0,1,"coq:exn.Nothing-to-rewrite","Nothing to rewrite"],[5,4,1,"coq:flag.Nra-Cache","Nra Cache"],[71,3,1,"coq:cmd.Number-Notation","Number Notation"],[9,3,1,"coq:cmd.Obligation","Obligation"],[9,3,1,"coq:cmd.Obligation-Tactic","Obligation Tactic"],[9,3,1,"coq:cmd.Obligations","Obligations"],[64,3,1,"coq:cmd.Opaque","Opaque"],[71,3,1,"coq:cmd.Open-Scope","Open Scope"],[66,3,1,"coq:cmd.Optimize-Heap","Optimize Heap"],[66,3,1,"coq:cmd.Optimize-Proof","Optimize Proof"],[28,3,1,"coq:cmd.Parameter","Parameter"],[28,3,1,"coq:cmd.Parameters","Parameters"],[44,4,1,"coq:flag.Parsing-Explicit","Parsing Explicit"],[14,7,1,"coq:attr.Polymorphic","Polymorphic"],[14,4,1,"coq:flag.Polymorphic-Inductive-Cumulativity","Polymorphic Inductive Cumulativity"],[14,0,1,"coq:exn.Polymorphic-universe-constraints-can-only-be-declared-inside-sections,-use-Monomorphic-Constraint-instead","Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead"],[14,0,1,"coq:exn.Polymorphic-universes-can-only-be-declared-inside-sections,-use-Monomorphic-Universe-instead","Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead"],[59,4,1,"coq:flag.Positivity-Checking","Positivity Checking"],[57,3,1,"coq:cmd.Prenex-Implicits","Prenex Implicits"],[9,3,1,"coq:cmd.Preterm","Preterm"],[59,3,1,"coq:cmd.Primitive","Primitive"],[37,4,1,"coq:flag.Primitive-Projections","Primitive Projections"],[59,3,1,"coq:cmd.Print","Print"],[59,3,1,"coq:cmd.Print-All","Print All"],[59,3,1,"coq:cmd.Print-All-Dependencies","Print All Dependencies"],[59,3,1,"coq:cmd.Print-Assumptions","Print Assumptions"],[42,3,1,"coq:cmd.Print-Canonical-Projections","Print Canonical Projections"],[4,3,1,"coq:cmd.Print-Classes","Print Classes"],[4,3,1,"coq:cmd.Print-Coercion-Paths","Print Coercion Paths"],[4,3,1,"coq:cmd.Print-Coercions","Print Coercions"],[71,3,1,"coq:cmd.Print-Custom-Grammar","Print Custom Grammar"],[66,3,1,"coq:cmd.Print-Debug-GC","Print Debug GC"],[64,3,1,"coq:cmd.Print-Equivalent-Keys","Print Equivalent Keys"],[2,3,1,"coq:cmd.Print-Extraction-Blacklist","Print Extraction Blacklist"],[2,3,1,"coq:cmd.Print-Extraction-Callback","Print Extraction Callback"],[2,3,1,"coq:cmd.Print-Extraction-Foreign","Print Extraction Foreign"],[2,3,1,"coq:cmd.Print-Extraction-Inline","Print Extraction Inline"],[11,3,1,"coq:cmd.Print-Fields","Print Fields"],[62,3,1,"coq:cmd.Print-Firstorder-Solver","Print Firstorder Solver"],[71,3,1,"coq:cmd.Print-Grammar","Print Grammar"],[4,3,1,"coq:cmd.Print-Graph","Print Graph"],[60,3,1,"coq:cmd.Print-Hint","Print Hint"],[60,3,1,"coq:cmd.Print-HintDb","Print HintDb"],[44,3,1,"coq:cmd.Print-Implicit","Print Implicit"],[13,3,1,"coq:cmd.Print-Instances","Print Instances"],[71,3,1,"coq:cmd.Print-Keywords","Print Keywords"],[59,3,1,"coq:cmd.Print-Libraries","Print Libraries"],[59,3,1,"coq:cmd.Print-LoadPath","Print LoadPath"],[54,3,1,"coq:cmd.Print-Ltac","Print Ltac"],[54,3,1,"coq:cmd.Print-Ltac-Signatures","Print Ltac Signatures"],[55,3,1,"coq:cmd.Print-Ltac2","Print Ltac2"],[55,3,1,"coq:cmd.Print-Ltac2-Signatures","Print Ltac2 Signatures"],[55,3,1,"coq:cmd.Print-Ltac2-Type","Print Ltac2 Type"],[59,3,1,"coq:cmd.Print-ML-Modules","Print ML Modules"],[59,3,1,"coq:cmd.Print-ML-Path","Print ML Path"],[35,3,1,"coq:cmd.Print-Module","Print Module"],[35,3,1,"coq:cmd.Print-Module-Type","Print Module Type"],[35,3,1,"coq:cmd.Print-Namespace","Print Namespace"],[71,3,1,"coq:cmd.Print-Notation","Print Notation"],[59,3,1,"coq:cmd.Print-Opaque-Dependencies","Print Opaque Dependencies"],[29,3,1,"coq:cmd.Print-Options","Print Options"],[59,3,1,"coq:cmd.Print-Registered","Print Registered"],[59,3,1,"coq:cmd.Print-Registered-Schemes","Print Registered Schemes"],[60,3,1,"coq:cmd.Print-Rewrite-HintDb","Print Rewrite HintDb"],[11,3,1,"coq:cmd.Print-Rings","Print Rings"],[71,3,1,"coq:cmd.Print-Scope","Print Scope"],[71,3,1,"coq:cmd.Print-Scopes","Print Scopes"],[59,3,1,"coq:cmd.Print-Section","Print Section"],[64,3,1,"coq:cmd.Print-Strategies","Print Strategies"],[64,3,1,"coq:cmd.Print-Strategy","Print Strategy"],[29,3,1,"coq:cmd.Print-Table","Print Table"],[29,3,1,"coq:cmd.Print-Tables","Print Tables"],[59,3,1,"coq:cmd.Print-Transparent-Dependencies","Print Transparent Dependencies"],[13,3,1,"coq:cmd.Print-Typeclasses","Print Typeclasses"],[59,3,1,"coq:cmd.Print-Typing-Flags","Print Typing Flags"],[14,3,1,"coq:cmd.Print-Universes","Print Universes"],[71,3,1,"coq:cmd.Print-Visibility","Print Visibility"],[59,4,1,"coq:flag.Printing-All","Printing All"],[46,4,1,"coq:flag.Printing-Allow-Match-Default-Clause","Printing Allow Match Default Clause"],[4,8,1,"coq:table.Printing-Coercion","Printing Coercion"],[4,4,1,"coq:flag.Printing-Coercions","Printing Coercions"],[59,4,1,"coq:flag.Printing-Compact-Contexts","Printing Compact Contexts"],[37,8,1,"coq:table.Printing-Constructor","Printing Constructor"],[59,4,1,"coq:flag.Printing-Dependent-Evars-Line","Printing Dependent Evars Line"],[59,6,1,"coq:opt.Printing-Depth","Printing Depth"],[43,4,1,"coq:flag.Printing-Existential-Instances","Printing Existential Instances"],[46,4,1,"coq:flag.Printing-Factorizable-Match-Patterns","Printing Factorizable Match Patterns"],[27,4,1,"coq:flag.Printing-Float","Printing Float"],[66,4,1,"coq:flag.Printing-Goal-Names","Printing Goal Names"],[66,4,1,"coq:flag.Printing-Goal-Tags","Printing Goal Tags"],[46,8,1,"coq:table.Printing-If","Printing If"],[44,4,1,"coq:flag.Printing-Implicit","Printing Implicit"],[44,4,1,"coq:flag.Printing-Implicit-Defensive","Printing Implicit Defensive"],[46,8,1,"coq:table.Printing-Let","Printing Let"],[46,4,1,"coq:flag.Printing-Match-All-Subterms","Printing Match All Subterms"],[46,4,1,"coq:flag.Printing-Matching","Printing Matching"],[71,4,1,"coq:flag.Printing-Notations","Printing Notations"],[71,4,1,"coq:flag.Printing-Parentheses","Printing Parentheses"],[37,4,1,"coq:flag.Printing-Primitive-Projection-Parameters","Printing Primitive Projection Parameters"],[37,4,1,"coq:flag.Printing-Projections","Printing Projections"],[71,4,1,"coq:flag.Printing-Raw-Literals","Printing Raw Literals"],[37,8,1,"coq:table.Printing-Record","Printing Record"],[37,4,1,"coq:flag.Printing-Records","Printing Records"],[12,4,1,"coq:flag.Printing-Relevance-Marks","Printing Relevance Marks"],[46,4,1,"coq:flag.Printing-Synth","Printing Synth"],[59,4,1,"coq:flag.Printing-Unfocused","Printing Unfocused"],[37,4,1,"coq:flag.Printing-Unfolded-Projection-As-Match","Printing Unfolded Projection As Match"],[14,4,1,"coq:flag.Printing-Universes","Printing Universes"],[44,4,1,"coq:flag.Printing-Use-Implicit-Types","Printing Use Implicit Types"],[59,6,1,"coq:opt.Printing-Width","Printing Width"],[46,4,1,"coq:flag.Printing-Wildcard","Printing Wildcard"],[40,7,1,"coq:attr.Private","Private"],[14,4,1,"coq:flag.Private-Polymorphic-Universes","Private Polymorphic Universes"],[59,3,1,"coq:cmd.Profile","Profile"],[9,7,1,"coq:attr.Program","Program"],[9,4,1,"coq:flag.Program-Cases","Program Cases"],[9,4,1,"coq:flag.Program-Generalized-Coercion","Program Generalized Coercion"],[9,4,1,"coq:flag.Program-Mode","Program Mode"],[66,3,1,"coq:cmd.Proof","Proof"],[66,3,1,"coq:cmd.Proof-Mode","Proof Mode"],[66,3,1,"coq:cmd.Proof-`term`","Proof `term`"],[66,3,1,"coq:cmd.Proof-using","Proof using"],[60,3,1,"coq:cmd.Proof-with","Proof with"],[32,3,1,"coq:cmd.Property","Property"],[32,3,1,"coq:cmd.Proposition","Proposition"],[5,5,1,"coq:thm.Psatz","Psatz"],[2,3,1,"coq:cmd.Pwd","Pwd"],[66,3,1,"coq:cmd.Qed","Qed"],[59,3,1,"coq:cmd.Quit","Quit"],[37,3,1,"coq:cmd.Record","Record"],[37,0,1,"coq:exn.Records-declared-with-the-keyword-Record-or-Structure-cannot-be-recursive","Records declared with the keyword Record or Structure cannot be recursive"],[2,3,1,"coq:cmd.Recursive-Extraction","Recursive Extraction"],[2,3,1,"coq:cmd.Recursive-Extraction-Library","Recursive Extraction Library"],[59,3,1,"coq:cmd.Redirect","Redirect"],[59,3,1,"coq:cmd.Register","Register"],[59,3,1,"coq:cmd.Register-Inline","Register Inline"],[59,3,1,"coq:cmd.Register-Scheme","Register Scheme"],[64,4,1,"coq:flag.Regular-Subst-Tactic","Regular Subst Tactic"],[32,3,1,"coq:cmd.Remark","Remark"],[29,3,1,"coq:cmd.Remove","Remove"],[60,3,1,"coq:cmd.Remove-Hints","Remove Hints"],[59,3,1,"coq:cmd.Require","Require"],[59,3,1,"coq:cmd.Require-Export","Require Export"],[59,3,1,"coq:cmd.Require-Import","Require Import"],[71,3,1,"coq:cmd.Reserved-Infix","Reserved Infix"],[71,3,1,"coq:cmd.Reserved-Notation","Reserved Notation"],[59,3,1,"coq:cmd.Reset","Reset"],[2,3,1,"coq:cmd.Reset-Extraction-Blacklist","Reset Extraction Blacklist"],[2,3,1,"coq:cmd.Reset-Extraction-Callback","Reset Extraction Callback"],[2,3,1,"coq:cmd.Reset-Extraction-Inline","Reset Extraction Inline"],[59,3,1,"coq:cmd.Reset-Initial","Reset Initial"],[54,3,1,"coq:cmd.Reset-Ltac-Profile","Reset Ltac Profile"],[66,3,1,"coq:cmd.Restart","Restart"],[44,4,1,"coq:flag.Reversible-Pattern-Implicit","Reversible Pattern Implicit"],[10,3,1,"coq:cmd.Rewrite-Rule","Rewrite Rule"],[10,3,1,"coq:cmd.Rewrite-Rules","Rewrite Rules"],[10,0,1,"coq:exn.Rewrite-rule-declaration-requires-passing-the-flag-\"-allow-rewrite-rules\"","Rewrite rule declaration requires passing the flag "-allow-rewrite-rules""],[67,4,1,"coq:flag.Rewriting-Schemes","Rewriting Schemes"],[11,0,1,"coq:exn.Ring-operation-should-be-declared-as-a-morphism","Ring operation should be declared as a morphism"],[12,0,1,"coq:exn.SProp-is-disallowed-because-the-\"Allow-StrictProp\"-flag-is-off","SProp is disallowed because the "Allow StrictProp" flag is off"],[66,3,1,"coq:cmd.Save","Save"],[67,3,1,"coq:cmd.Scheme","Scheme"],[67,3,1,"coq:cmd.Scheme-Boolean-Equality","Scheme Boolean Equality"],[67,3,1,"coq:cmd.Scheme-Equality","Scheme Equality"],[71,0,1,"coq:exn.Scope-delimiters-should-not-start-with-an-underscore","Scope delimiters should not start with an underscore"],[71,0,1,"coq:exn.Scope-names-should-not-start-with-an-underscore","Scope names should not start with an underscore"],[59,3,1,"coq:cmd.Search","Search"],[59,8,1,"coq:table.Search-Blacklist","Search Blacklist"],[59,4,1,"coq:flag.Search-Output-Name-Only","Search Output Name Only"],[59,3,1,"coq:cmd.SearchPattern","SearchPattern"],[59,3,1,"coq:cmd.SearchRewrite","SearchRewrite"],[38,3,1,"coq:cmd.Section","Section"],[64,0,1,"coq:exn.Section-variable-\u2018ident\u2019-occurs-implicitly-in-global-declaration-\u2018qualid\u2019-present-in-hypothesis-\u2018ident\u2019","Section variable \u2018ident\u2019 occurs implicitly in global declaration \u2018qualid\u2019 present in hypothesis \u2018ident\u2019"],[64,0,1,"coq:exn.Section-variable-\u2018ident\u2019-occurs-implicitly-in-global-declaration-\u2018qualid\u2019-present-in-the-conclusion","Section variable \u2018ident\u2019 occurs implicitly in global declaration \u2018qualid\u2019 present in the conclusion"],[2,3,1,"coq:cmd.Separate-Extraction","Separate Extraction"],[29,3,1,"coq:cmd.Set","Set"],[35,4,1,"coq:flag.Short-Module-Printing","Short Module Printing"],[66,3,1,"coq:cmd.Show","Show"],[66,3,1,"coq:cmd.Show-Conjectures","Show Conjectures"],[66,3,1,"coq:cmd.Show-Existentials","Show Existentials"],[2,3,1,"coq:cmd.Show-Extraction","Show Extraction"],[66,3,1,"coq:cmd.Show-Goal","Show Goal"],[66,3,1,"coq:cmd.Show-Intro","Show Intro"],[66,3,1,"coq:cmd.Show-Intros","Show Intros"],[5,3,1,"coq:cmd.Show-Lia-Profile","Show Lia Profile"],[54,3,1,"coq:cmd.Show-Ltac-Profile","Show Ltac Profile"],[66,3,1,"coq:cmd.Show-Match","Show Match"],[9,3,1,"coq:cmd.Show-Obligation-Tactic","Show Obligation Tactic"],[66,3,1,"coq:cmd.Show-Proof","Show Proof"],[66,3,1,"coq:cmd.Show-Universes","Show Universes"],[5,3,1,"coq:cmd.Show-Zify","Show Zify"],[35,0,1,"coq:exn.Signature-components-for-field-\u2018ident\u2019-do-not-match","Signature components for field \u2018ident\u2019 do not match"],[59,4,1,"coq:flag.Silent","Silent"],[9,3,1,"coq:cmd.Solve-All-Obligations","Solve All Obligations"],[9,3,1,"coq:cmd.Solve-Obligations","Solve Obligations"],[66,4,1,"coq:flag.Solve-Unification-Constraints","Solve Unification Constraints"],[57,4,1,"coq:flag.SsrHave-NoTCResolution","SsrHave NoTCResolution"],[57,4,1,"coq:flag.SsrIdents","SsrIdents"],[57,4,1,"coq:flag.SsrOldRewriteGoalsOrder","SsrOldRewriteGoalsOrder"],[57,4,1,"coq:flag.SsrRewrite","SsrRewrite"],[71,2,1,"coq:warn.Stack-overflow-or-segmentation-fault-happens-when-working-with-large-numbers-in-\u2018type\u2019-(threshold-may-vary-depending-on-your-system-limits-and-on-the-command-executed)","Stack overflow or segmentation fault happens when working with large numbers in \u2018type\u2019 (threshold may vary depending on your system limits and on the command executed)"],[64,3,1,"coq:cmd.Strategy","Strategy"],[44,4,1,"coq:flag.Strict-Implicit","Strict Implicit"],[14,4,1,"coq:flag.Strict-Universe-Declaration","Strict Universe Declaration"],[71,3,1,"coq:cmd.String-Notation","String Notation"],[44,4,1,"coq:flag.Strongly-Strict-Implicit","Strongly Strict Implicit"],[67,4,1,"coq:flag.Structural-Injection","Structural Injection"],[37,3,1,"coq:cmd.Structure","Structure"],[4,3,1,"coq:cmd.SubClass","SubClass"],[59,3,1,"coq:cmd.Succeed","Succeed"],[66,4,1,"coq:flag.Suggest-Proof-Using","Suggest Proof Using"],[10,3,1,"coq:cmd.Symbol","Symbol"],[10,3,1,"coq:cmd.Symbols","Symbols"],[71,0,1,"coq:exn.Syntax-error:-[prim:reference]-expected-after-'Notation'-(in-[vernac:command])","Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command])"],[71,0,1,"coq:exn.Syntax-error:-[prim:reference]-expected-after-[prim:reference]-(in-[vernac:command])","Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command])"],[71,3,1,"coq:cmd.Tactic-Notation","Tactic Notation"],[54,0,1,"coq:exn.Tactic-failure","Tactic failure"],[54,0,1,"coq:exn.Tactic-failure-(level-\u2018natural\u2019)","Tactic failure (level \u2018natural\u2019)"],[54,0,1,"coq:exn.Tactic-failure:-match
construct","Setting properties of a function's arguments","Canonical Structures","Existential variables","Implicit arguments","Language extensions","Extended pattern matching","<no title>","<no title>","<no title>","<no title>","The Rocq Prover commands","CoqIDE","Building Rocq Projects","Ltac","Ltac2","<no title>","The SSReflect proof language","Tactics","Commands","Programmable proof search","Automatic solvers and programmable tactics","Solvers for logic and equality","Creating new tactics","Reasoning with equalities","Basic proof writing","Proof mode","Reasoning with inductive types","<no title>","Glossary index","<no title>","Syntax extensions and notation scopes","Functional induction","Libraries and plugins","Writing Rocq libraries and plugins","Documenting Rocq files with coqdoc","Command-line and graphical tools","Bibliography"],titleterms:{"0":[17,24],"0beta":17,"1":[17,24,37,67],"10":17,"11":17,"12":17,"13":17,"14":17,"15":17,"16":17,"17":17,"18":17,"19":17,"1beta":17,"1gamma":17,"2":[17,24,37,67],"20":17,"3":[17,24,71],"4":[17,24],"4beta":17,"4beta2":17,"5":[17,24],"5beta1":17,"5beta2":17,"5beta3":17,"5pl1":17,"5pl2":17,"5pl3":17,"6":[17,24],"6beta1":17,"7":[17,24],"8":17,"9":17,"\u03b1":31,"\u03b2":31,"\u03b4":31,"\u03b6":31,"\u03b7":31,"\u03b9":31,"abstract":[57,66],"boolean":[46,54,57],"byte":36,"case":[5,24,40,52,57,58,67],"catch":[54,55],"class":[3,4,37,55,71],"default":[41,46],"do":[11,54],"float":[27,36],"function":[4,28,30,34,41,44,54,60,72],"long":24,"new":[3,11,17,24,35,53,57,63],"short":5,"static":55,"switch":[55,57],"try":54,A:[2,14,35,58,67],In:55,Is:11,No:53,One:57,The:[11,26,27,34,35,44,51,53,57,71,75],_coqproject:53,abbrevi:[55,57,71],about:[7,46,71],access:37,ackermann:60,acknowledg:57,activ:4,ad:[3,11,52],addit:[2,57,60],advanc:[57,72],algorithm:64,alia:74,alias:46,altern:[41,54],alwai:64,ambigu:3,an:[35,57,59,67],analysi:67,annot:8,anonym:[37,57],antiquot:55,api:55,appendix:25,appli:[43,57,58,64,67],applic:[4,28,44,54,58],ar:[57,66],argument:[2,37,41,44,46,53,57,67,71],arithmet:[5,27],ariti:34,arrai:36,ask:9,assert:32,assert_fail:54,assert_succe:54,assign:57,associ:71,assumpt:[28,57],asynchron:[8,52],attribut:[4,17,18,29,35,38],autom:60,automat:[8,11,34,41,43,44,61,67],avail:4,avoid:2,axiom:2,b:58,backtrac:54,backtrack:[54,55,59],backward:[3,58],base:36,basic:[12,27,29,52,53,54,57,65,71],batch:51,beta1:17,beta2:17,beta3:17,beta:31,between:[2,55,59,66],bibliographi:77,bidirection:41,bind:[13,41,52,55,58,71],binder:[3,28,44,57,71],block:[8,57],bookkeep:57,both:71,bound:71,brace:66,branch:[54,57],breakpoint:52,buffer:52,build:[13,53],built:55,bullet:[57,66],calcul:66,calculu:26,call:[52,55],can:43,canon:42,cast:32,casual:44,caveat:[8,30],cell:55,chain:57,chang:[15,17,24,55],charact:52,check:54,checker:51,classic:58,claus:[37,46,58],clear:57,co:30,code:2,coercion:[4,46,71],cofix:30,coinduct:30,combin:[44,58,67],command:[3,13,17,19,24,35,51,52,57,59,66,67,71,75,76],comment:53,common:[53,58],compact:42,comparison:[54,55],compat:[10,17,37,55,57,74],compil:[17,51,52,53,59],complex:71,compon:55,compound:58,comput:[53,54,64],conclus:59,concret:[11,24],condit:[34,54,57],configur:53,conflict:2,confluenc:10,congruenc:57,connect:27,constant:[3,37,59,71],constraint:[14,66],construct:[12,24,26,34,37,40,54,59],constructor:[34,67],content:25,context:[3,13,54,55,57,58],contextu:[44,57],continu:[3,41,44],contradict:58,contravari:3,contribut:[2,24,27],control:[9,35,44,46,54,57,58,59,64,66],convent:[29,46],convers:[14,31,64],convert:31,coq:[24,27,52],coq_makefil:53,coqc:[51,53],coqchk:51,coqdep:53,coqdoc:75,coqid:[17,52],coqmakefil:53,coqrc:51,coqtop:51,core:33,corecurs:30,correct:34,count:54,covari:3,creat:[35,37,43,60,63],cumul:14,curli:66,custom:[51,52,71],cut:[5,54],cycl:66,databas:60,datatyp:27,deactiv:44,deal:11,debug:[12,54,55,59],debugg:[52,54],decid:[54,67],decis:5,declar:[3,13,38,41,42,44,55,57,66,67],defect:[54,57],defin:[10,34,35,37,54,55,60],definit:[3,9,12,14,30,32,34,37,40,46,54,55,57,64,71],delai:[55,66],delta:31,demonstr:14,depend:[17,46,53,58,59,67],deprec:[3,74],deriv:[6,42,67],descript:5,design:55,destruct:67,destructor:34,destructur:[46,57],detail:[2,17,24,53],detect:54,diff:66,differ:[2,44,66],disabl:71,disambigu:59,discharg:57,discrimin:67,discuss:11,disjunct:46,displai:[4,43,44,52,59,71],divis:2,document:[29,53,75],doe:[11,46],doesn:64,domain:7,dune:53,dynam:55,e:43,eappli:43,earli:24,eauto:13,edit:52,effect:[41,55],effici:24,elabor:9,element:[54,58],elim:57,elimin:[2,46,57],embed:53,emphasi:75,enabl:[3,66,71],encod:[12,52],end:[34,38],enter:66,entri:[57,71],environ:[51,59],equal:[7,9,27,62,64,67],equat:[11,57],equival:[57,58],error:[8,20,54,55],escap:75,essenti:29,eta:10,euclidean:2,eval:[54,64],evalu:[54,55],even:67,exact:57,exactly_onc:54,exampl:[2,3,4,5,6,11,14,17,26,27,28,29,30,31,34,35,37,38,40,41,42,43,44,46,51,52,53,54,55,57,58,59,60,62,64,66,67,71,72,74,75],except:55,execut:54,exist:[2,24,35],existenti:[43,57],exit:66,expans:[31,46],explicit:[14,43,44,57],explicitli:44,expos:59,express:[46,54,55,71],extend:[46,57],extens:[3,24,45,46,57,71],extra:[2,59],extract:[2,17,24],factor:[46,71],fail:[46,54,57],failur:54,famili:57,fast:[59,64],fatal:55,ffi:2,field:[11,35,37],file:[51,52,53,59,74,75],filenam:[2,53],fill:54,first:[3,34,46,54,57],fix:[31,34],fixpoint:[9,34],flag:[17,21,29,59],flow:[54,57,58],focus:[54,66],fold:64,fold_right:64,follow:44,foral:28,forbidden:53,forest:67,form:34,forward:58,found:27,frequent:9,fresh:54,from:[35,44,55],full:59,fun:28,function_scop:71,functor:35,gallina:57,gener:[2,3,4,11,14,23,29,44,54,55,57,67,71,72],get:[54,57],give:44,given:34,global:[14,54,71],glossari:69,goal:[5,11,54,55,57,58,66,67],grammar:[24,53],graph:4,graphic:76,guard:54,hand:46,have:[54,57],helper:67,hidden:46,hide:75,hierarchi:[13,42],high:5,higher:10,hint:[41,57,59,60],histor:24,histori:[11,15,24],hole:[10,54],horror:2,how:[11,66],html:75,hyperlink:75,hypothes:[54,55,58,59,66],hypothesi:[54,58],ident:[4,54],identifi:[59,71],idtac:54,implicit:[4,41,44,46,60,71],implicits_alt:41,impred:26,includ:58,incompat:[3,17],indent:57,index:[16,18,19,20,21,22,23,34,57,69],induct:[2,26,34,40,46,67,71,72],infer:[17,43,44],infix:71,inform:[66,71],infrastructur:17,inherit:[4,71],inlin:[2,59],innermost:3,input:52,insert:44,insid:[53,54,75],instal:53,instanc:[13,43],integ:[5,27,36,71],integr:7,interact:[8,35,44,51,54,55,57],interdepend:53,interfac:51,intern:59,interpret:[57,71],intro:[57,58],introduc:74,introduct:[3,25,57],intuitionist:54,invers:67,inversion_sigma:67,invoc:58,involv:[46,71],io:55,irrefut:46,irrelev:[12,31],is_cofix:54,is_fix:54,is_proj:54,isomorph:54,issu:[12,17,57],item:[35,57],iter:57,j:53,kei:52,kernel:17,keyword:[58,59],kind:44,knowledg:44,languag:[2,17,24,25,33,45,55,57],larger:67,late:53,latex:[53,75],launch:51,law:10,layer:55,lazy_match:55,lazymatch:54,least:54,left:67,leibniz:64,lemma:[9,27,66],let:[24,32,46,54,57],level:[5,10,29,30,32,34,55],lexic:29,lia:5,librari:[17,24,27,51,53,59,60,71,73,74],licit:57,limit:67,line:[17,51,75,76],linear:5,liner:57,list:[27,54,55,75],load:[51,53,59],local:[14,29,35,38,46,53,54,57,58,60,71],locat:[59,71],lock:57,logic:[27,53,54,60,62],loop:54,low:55,lower:34,lra:5,ltac1:55,ltac2:[17,55],ltac:[17,54,55],maccarthi:60,machin:59,macro:54,main:24,mainten:66,make:54,man:53,manag:[52,58,66],manipul:54,manual:[17,41,44],map:11,match:[31,34,37,40,46,54,55,57],materi:75,maxim:44,mechan:57,memori:66,meta:55,metavari:57,micromega:5,minim:14,miscellan:[17,24],ml:[2,55],mode:[8,44,52,55,57,66],modifi:53,modul:[4,35,53],monomorph:14,more:7,morphism:3,move:[57,58],multi:57,multi_match:55,multimatch:54,multipl:[37,41,46,53,54,55,57],museum:2,must:46,mutabl:55,mutual:34,n:67,name:[24,35,37,54,66],nat:[27,29],nativ:[17,53],native_comput:[53,64],natur:[54,55,60,67],neg:34,nest:[34,46],nia:5,non:[5,12,34,44,54,55,58,67,71],noncumul:14,nonreflex:3,nonsymmetr:3,notat:[17,27,42,54,55,59,71],notion:29,novelti:24,nra:5,nsatz:7,number:[27,54,60,71],numgoal:54,object:[34,36,46,74],oblig:9,ocaml:59,occurr:[34,57,58,67],odd:67,old:17,omit:35,onc:54,opam:53,opaqu:13,open:71,oper:59,optim:[2,54],option:[2,17,21,29,51,66,75],or_and_intropattern:67,order:[5,10,58],orient:58,other:[17,44,66],outermost:3,over:[5,9,55,57],overflow:29,overload:42,overview:[53,55],own:53,packag:53,page:53,parallel:8,paramet:[35,46,51,57],parameter:[13,34,71],parametr:[3,46,57],pars:[24,44,55,71],part:[59,75],partial:58,path:[53,59],pattern:[10,44,46,54,55,57,58,59,71],peano:27,perform:[53,58],permut:54,phrase:53,plane:5,plugin:[73,74],polymorph:[10,14,34,57],polynomi:11,posit:34,positivstellensatz:5,potenti:17,pre:5,preced:71,precompil:53,predefin:71,predic:[46,57,67],prefer:52,prelud:27,premis:[58,67],present:[4,14],preserv:10,pretti:[43,44,46,75],primit:[27,36,37,59,71],principl:[67,72,75],print:[3,4,14,37,43,44,46,54,55,59,71,75],privat:40,procedur:5,process:[5,8,54],produc:51,product:58,profil:[51,54,55],program:[2,6,9,27,55,60],programm:[60,61],progress:54,project:[37,53],proof:[5,8,12,14,25,31,32,46,54,57,58,60,65,66],prop:34,properti:[41,54,71],proposit:[12,27,54],prove:[54,66,67],prover:[25,51,53],provid:[3,46],psatz:5,qualifi:35,quantifi:27,queri:[52,59],question:9,quit:59,quot:53,quotat:55,radix:71,ration:[5,11],real:[5,17,27],realiz:2,reason:[58,64,67],recent:[15,17],record:[4,37],recurr:57,recurs:[27,30,34,55,71,72],redex:57,reduct:[24,31,34,37,55,59,64],refer:[17,54,59],reflect:57,refut:5,regist:59,registr:59,relat:3,remark:57,renam:41,reorder:[54,66],repeat:54,repetit:57,request:[59,66],reserv:[58,71],resili:8,resolut:[43,44,57],reus:37,revers:[4,44,54,55,64],revgoal:66,rewrit:[3,10,57,64,67],right:[46,67],ring:[5,11],rocq:[2,25,51,53,57,60,71,74,75],root:[24,53],rule:[10,26,31,34,38,57,64,71,75],run:[52,54],s:[2,27,41,67],same:[46,53],save:52,scheme:[67,72],scheme_typ:67,scope:[35,41,71],script:[51,52],search:[59,60],searchpattern:59,searchrewrit:59,second:[34,46,54,58],section:[4,13,14,38,66,75],select:57,selector:[54,57],semant:55,separ:66,sequenc:54,set:[2,13,26,29,37,41,57,58,60,66],setoid:[3,64],setup:53,share:35,shelv:66,shelve_unifi:66,shortcut:57,show:[66,75],side:[11,46],simpl:[28,31,34,35,55,64,71],simple_bind:58,simplif:57,simultan:71,singl:[51,54],soft:54,solv:[9,43,54,66],solver:[5,7,11,61,62],some:[2,27,35],sort:[14,34,39],sourc:[17,75],special:[57,58],specif:[17,25,27],specifi:14,split:[5,53],sprop:12,ssreflect:[17,57],stack:[29,52],standard:[17,24,27,55,57,60,71],start:[51,57],state:66,statu:59,step:[57,66],strategi:[3,46,64],strict:[12,34,44,55],strictli:34,string:[27,36,71],structur:[11,42,57],style:75,sub:35,subgoal:66,subpattern:46,subrel:3,subset:53,substitut:54,substructur:13,subterm:[43,46],subtyp:[26,44],succe:54,success:54,suff:57,suggest:8,summari:[13,17,24,35,38],superclass:13,support:[10,29,52],survei:27,swap:66,symbol:[10,52,54],synopsi:57,syntact:[9,54,55],syntax:[3,10,17,24,29,44,46,54,55,57,71],system:[2,35],t:64,tabl:[21,29],tactic:[3,5,11,17,22,24,27,43,54,55,57,58,60,61,63,64,67,71,72,74],target:[2,53],templat:[34,52],term:[26,54,55,64,71],termin:[10,12,57],test:[53,54],theorem:58,theori:34,thi:11,time:[51,53,54],time_constr:54,timeout:54,tool:[17,24,76],top:[30,32,34],toplevel:54,trace:54,trail:44,transit:55,transpar:13,tree:67,trigger:74,tryif:54,two:[35,54],type:[2,3,4,10,17,26,28,30,32,34,35,37,38,40,44,46,54,55,57,59,67,71],type_scop:71,type_term:54,typeclass:[13,57],uip:12,under:[3,57],understand:46,undo:64,unfold:[3,41,64],unicod:52,unif:[14,58,66],uninstal:53,univers:[10,14],unlock:57,unreleas:17,unset:29,until:58,untyp:54,unus:46,up:51,upgrad:53,us:[4,14,25,35,37,38,43,44,46,51,52,53,54,58,64,66,67,71],usag:[3,11,57,66,75],useless:2,user:[2,3,10,24,27],valu:[3,46,54,55],variabl:[11,43,44,46,51,52,55,66],varianc:14,variant:[40,46,57,58],variou:67,verbatim:75,version:[17,24,53],view:[5,57],vm_comput:64,vo:51,vocabulari:29,vs:[43,55,57],wai:[54,55],warn:[20,53,74],weak:14,well:[27,34],what:11,when:[44,46,57],wildcard:[46,57],wlog:57,work:[11,53,66],write:[46,65,74],your:53,zifi:5}})
\ No newline at end of file
diff --git a/master/stdlib/Stdlib.Arith.Arith_base.html b/master/stdlib/Stdlib.Arith.Arith_base.html
index 88a0392348..833a3d6f7d 100644
--- a/master/stdlib/Stdlib.Arith.Arith_base.html
+++ b/master/stdlib/Stdlib.Arith.Arith_base.html
@@ -58,7 +58,7 @@ Library Stdlib.Arith.Arith_base
Library Stdlib.Arith.Arith_base
Library Stdlib.Arith.EqNat
Equality on natural numbers
Propositional equality
+Propositional equality
Library Stdlib.Arith.PeanoNat
Remaining constants not defined in Stdlib.Init.Nat
+Remaining constants not defined in Stdlib.Init.Nat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Arith.PeanoNat
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Properties mixing andb and orb
+Properties mixing andb and orb
Library Stdlib.Bool.Bool
Library Stdlib.Bool.Bool
Reflection of bool into Prop
+Reflection of bool into Prop
Library Stdlib.Bool.Bool
Alternative versions of andb and orb
+Alternative versions of andb and orb
with lazy behavior (for vm_compute)
Library Stdlib.Bool.Bool
Reflect: a specialized inductive type for
+Reflect: a specialized inductive type for
relating propositions and booleans,
as popularized by the Ssreflect library.
diff --git a/master/stdlib/Stdlib.Bool.BoolOrder.html b/master/stdlib/Stdlib.Bool.BoolOrder.html
index cd3c5ac48f..9e5f9a6506 100644
--- a/master/stdlib/Stdlib.Bool.BoolOrder.html
+++ b/master/stdlib/Stdlib.Bool.BoolOrder.html
@@ -66,7 +66,7 @@ Library Stdlib.Bool.BoolOrder
Library Stdlib.Bool.BoolOrder
Library Stdlib.Bool.BoolOrder
Library Stdlib.Classes.CEquivalence
Typeclass-based setoids. Definitions on Equivalence.
+Typeclass-based setoids. Definitions on Equivalence.
Library Stdlib.Classes.CMorphisms
Typeclass-based morphism definition and standard, minimal instances
+Typeclass-based morphism definition and standard, minimal instances
Library Stdlib.Classes.CMorphisms
Morphisms.
+Morphisms.
Library Stdlib.Classes.CRelationClasses
Typeclass-based relations, tactics and standard instances
+Typeclass-based relations, tactics and standard instances
Library Stdlib.Classes.CRelationClasses
We can already dualize all these properties.
Standard instances.
+Standard instances.
Library Stdlib.Classes.CRelationClasses
Partial Order.
+Partial Order.
A partial order is a preorder which is additionally antisymmetric.
We give an equivalent definition, up-to an equivalence crelation
diff --git a/master/stdlib/Stdlib.Classes.DecidableClass.html b/master/stdlib/Stdlib.Classes.DecidableClass.html
index 760efce841..1f82fc6681 100644
--- a/master/stdlib/Stdlib.Classes.DecidableClass.html
+++ b/master/stdlib/Stdlib.Classes.DecidableClass.html
@@ -49,7 +49,7 @@ Library Stdlib.Classes.DecidableClass
A typeclass to ease the handling of decidable properties.
+A typeclass to ease the handling of decidable properties.
Library Stdlib.Classes.EquivDec
Decidable equivalences.
+Decidable equivalences.
Library Stdlib.Classes.Equivalence
Typeclass-based setoids. Definitions on Equivalence.
+Typeclass-based setoids. Definitions on Equivalence.
Library Stdlib.Classes.Init
Initialization code for typeclasses, setting up the default tactic
+Initialization code for typeclasses, setting up the default tactic
for instance search.
diff --git a/master/stdlib/Stdlib.Classes.Morphisms.html b/master/stdlib/Stdlib.Classes.Morphisms.html
index e4e170ce82..259c10485e 100644
--- a/master/stdlib/Stdlib.Classes.Morphisms.html
+++ b/master/stdlib/Stdlib.Classes.Morphisms.html
@@ -49,7 +49,7 @@ Library Stdlib.Classes.Morphisms
Typeclass-based morphism definition and standard, minimal instances
+Typeclass-based morphism definition and standard, minimal instances
Library Stdlib.Classes.Morphisms
Morphisms.
+Morphisms.
Library Stdlib.Classes.Morphisms_Prop
Proper instances for propositional connectives.
+Proper instances for propositional connectives.
Library Stdlib.Classes.Morphisms_Relations
Morphism instances for relations.
+Morphism instances for relations.
Library Stdlib.Classes.RelationClasses
Typeclass-based relations, tactics and standard instances
+Typeclass-based relations, tactics and standard instances
Library Stdlib.Classes.RelationClasses
We can already dualize all these properties.
Standard instances.
+Standard instances.
Library Stdlib.Classes.RelationClasses
Partial Order.
+Partial Order.
A partial order is a preorder which is additionally antisymmetric.
We give an equivalent definition, up-to an equivalence relation
diff --git a/master/stdlib/Stdlib.Classes.RelationPairs.html b/master/stdlib/Stdlib.Classes.RelationPairs.html
index a8d8da293d..680db6cf8d 100644
--- a/master/stdlib/Stdlib.Classes.RelationPairs.html
+++ b/master/stdlib/Stdlib.Classes.RelationPairs.html
@@ -49,7 +49,7 @@ Library Stdlib.Classes.RelationPairs
Library Stdlib.Classes.SetoidClass
Typeclass-based setoids, tactics and standard instances.
+Typeclass-based setoids, tactics and standard instances.
Library Stdlib.Classes.SetoidDec
Decidable setoid equality theory.
+Decidable setoid equality theory.
Library Stdlib.Classes.SetoidTactics
Tactics for typeclass-based setoids.
+Tactics for typeclass-based setoids.
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Extraction of minimum binding
+Extraction of minimum binding
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Basic results about MapsTo, In, lt_tree, gt_tree, height
+Basic results about MapsTo, In, lt_tree, gt_tree, height
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Library Stdlib.FSets.FMapAVL
Encapsulation
+Encapsulation
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Relations between Equal, Equiv and Equivb.
+Relations between Equal, Equiv and Equivb.
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Same facts for self-contained weak sets and for full maps
+Same facts for self-contained weak sets and for full maps
Library Stdlib.FSets.FMapFacts
Additional Properties for weak maps
+Additional Properties for weak maps
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Induction principles about fold contributed by S. Lescuyer
+Induction principles about fold contributed by S. Lescuyer
Library Stdlib.FSets.FMapFacts
Additional properties of fold
+Additional properties of fold
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFacts
Emulation of some functions lacking in the interface
+Emulation of some functions lacking in the interface
Library Stdlib.FSets.FMapFacts
Same Properties for self-contained weak maps and for full maps
+Same Properties for self-contained weak maps and for full maps
Library Stdlib.FSets.FMapFacts
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
Library Stdlib.FSets.FMapFullAVL
As comparison function, we propose here a non-structural
+As comparison function, we propose here a non-structural
version faithful to the code of Ocaml's Map library, instead of
the structural version of FMapAVL
diff --git a/master/stdlib/Stdlib.FSets.FMapInterface.html b/master/stdlib/Stdlib.FSets.FMapInterface.html
index bbe3f611c5..272a468f94 100644
--- a/master/stdlib/Stdlib.FSets.FMapInterface.html
+++ b/master/stdlib/Stdlib.FSets.FMapInterface.html
@@ -49,7 +49,7 @@ Library Stdlib.FSets.FMapInterface
Weak signature for maps
+Weak signature for maps
Library Stdlib.FSets.FMapInterface
Static signature for Weak Maps
+Static signature for Weak Maps
Library Stdlib.FSets.FMapInterface
Library Stdlib.FSets.FMapInterface
Library Stdlib.FSets.FMapInterface
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapList
Library Stdlib.FSets.FMapPositive
FMapPositive : an implementation of FMapInterface for positive keys.
+FMapPositive : an implementation of FMapInterface for positive keys.
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FMapWeakList
Library Stdlib.FSets.FSetAVL
FSetAVL : Implementation of FSetInterface via AVL trees
+FSetAVL : Implementation of FSetInterface via AVL trees
Library Stdlib.FSets.FSetBridge
From non-dependent signature S to dependent signature Sdep.
+From non-dependent signature S to dependent signature Sdep.
Library Stdlib.FSets.FSetBridge
From dependent signature Sdep to non-dependent signature S.
+From dependent signature Sdep to non-dependent signature S.
Library Stdlib.FSets.FSetCompat
Compatibility functors between FSetInterface and MSetInterface.
+Compatibility functors between FSetInterface and MSetInterface.
Library Stdlib.FSets.FSetCompat
Library Stdlib.FSets.FSetCompat
Library Stdlib.FSets.FSetCompat
Library Stdlib.FSets.FSetCompat
Library Stdlib.FSets.FSetDecide
Overview
+Overview
This functor defines the tactic fsetdec, which will
solve any valid goal of the form
@@ -181,7 +181,7 @@ Library Stdlib.FSets.FSetDecide
Facts and Tactics for Propositional Logic
+Facts and Tactics for Propositional Logic
These lemmas and tactics are in a module so that they do
not affect the namespace if you import the enclosing
@@ -196,18 +196,18 @@ Library Stdlib.FSets.FSetDecide
Lemmas and Tactics About Decidable Propositions
+Lemmas and Tactics About Decidable Propositions
Propositional Equivalences Involving Negation
+Propositional Equivalences Involving Negation
These are all written with the unfolded form of
negation, since I am not sure if setoid rewriting will
always perform conversion.
Tactics for Negations
+Tactics for Negations
Library Stdlib.FSets.FSetDecide
Auxiliary Tactics
+Auxiliary Tactics
Again, these lemmas and tactics are in a module so that
they do not affect the namespace if you import the
@@ -471,7 +471,7 @@ Library Stdlib.FSets.FSetDecide
Generic Tactics
+Generic Tactics
We begin by defining a few generic, useful tactics.
Library Stdlib.FSets.FSetDecide
Discarding Irrelevant Hypotheses
+Discarding Irrelevant Hypotheses
We will want to clear the context of any
non-FSet-related hypotheses in order to increase the
@@ -668,7 +668,7 @@ Library Stdlib.FSets.FSetDecide
Turning Set Operators into Propositional Connectives
+Turning Set Operators into Propositional Connectives
The lemmas from FSetFacts will be used to break down
set operations into propositional formulas built over
@@ -694,7 +694,7 @@ Library Stdlib.FSets.FSetDecide
Decidability of FSet Propositions
+Decidability of FSet Propositions
Library Stdlib.FSets.FSetDecide
Normalizing Propositions About Equality
+Normalizing Propositions About Equality
We have to deal with the fact that E.eq may be
convertible with Coq's equality. Thus, we will find the
@@ -812,7 +812,7 @@ Library Stdlib.FSets.FSetDecide
Considering Decidability of Base Propositions
+Considering Decidability of Base Propositions
This tactic adds assertions about the decidability of
E.eq and In to the context. This is necessary for
@@ -861,7 +861,7 @@ Library Stdlib.FSets.FSetDecide
Handling Empty, Subset, and Equal
+Handling Empty, Subset, and Equal
This tactic instantiates universally quantified
hypotheses (which arise from the unfolding of Empty,
@@ -909,7 +909,7 @@ Library Stdlib.FSets.FSetDecide
The Core fsetdec Auxiliary Tactics
+The Core fsetdec Auxiliary Tactics
Library Stdlib.FSets.FSetDecide
The fsetdec Tactic
+The fsetdec Tactic
Here is the top-level tactic (the only one intended for
clients of this library). It's specification is given at
@@ -1065,7 +1065,7 @@ Library Stdlib.FSets.FSetDecide
Library Stdlib.FSets.FSetEqProperties
Finite sets library
+Finite sets library
Library Stdlib.FSets.FSetFacts
Library Stdlib.FSets.FSetFacts
Library Stdlib.FSets.FSetFacts
Library Stdlib.FSets.FSetInterface
Non-dependent signatures
+Non-dependent signatures
Library Stdlib.FSets.FSetInterface
programs together with axioms
Functorial signature for weak sets
+Functorial signature for weak sets
Library Stdlib.FSets.FSetInterface
Static signature for weak sets
+Static signature for weak sets
Library Stdlib.FSets.FSetInterface
Functorial signature for sets on ordered elements
+Functorial signature for sets on ordered elements
Library Stdlib.FSets.FSetInterface
Static signature for sets on ordered elements
+Static signature for sets on ordered elements
Library Stdlib.FSets.FSetInterface
Some subtyping tests
+Some subtyping tests
WSfun ---> WS
@@ -803,7 +803,7 @@
Library Stdlib.FSets.FSetInterface
Dependent signature
+Dependent signature
Library Stdlib.FSets.FSetList
Finite sets library
+Finite sets library
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Induction principles for fold (contributed by S. Lescuyer)
+Induction principles for fold (contributed by S. Lescuyer)
Library Stdlib.FSets.FSetProperties
Alternative (weaker) specifications for fold
+Alternative (weaker) specifications for fold
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Cardinal
+Cardinal
Characterization of cardinal in terms of fold
+Characterization of cardinal in terms of fold
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetProperties
Library Stdlib.FSets.FSetToFiniteSet
Finite sets library : conversion to old Finite_sets
+Finite sets library : conversion to old Finite_sets
Library Stdlib.FSets.FSetToFiniteSet
Going from FSets with usual Leibniz equality
+Going from FSets with usual Leibniz equality
to the good old Ensembles and Finite_sets theory.
Library Stdlib.FSets.FSetWeakList
Finite sets library
+Finite sets library
Library Stdlib.Floats.FloatAxioms
Properties of the primitive operators for the Binary64 format
+Properties of the primitive operators for the Binary64 format
Library Stdlib.Floats.FloatLemmas
Library Stdlib.Floats.FloatOps
Derived operations and mapping between primitive floats and spec_floats
+Derived operations and mapping between primitive floats and spec_floats
Library Stdlib.Floats.PrimFloat
Definition of the interface for primitive floating-point arithmetic
+Definition of the interface for primitive floating-point arithmetic
Library Stdlib.Floats.PrimFloat
IEEE 754-2008 standard.
Type definition for the co-domain of compare
+Type definition for the co-domain of compare
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.PrimFloat
Exponent manipulation functions
+Exponent manipulation functions
frshiftexp: convert a float to fractional part in [0.5, 1.)
and integer part.
Library Stdlib.Floats.PrimFloat
Predecesor/Successor functions
+Predecesor/Successor functions
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.PrimFloat
Library Stdlib.Floats.SpecFloat
Specification of floating-point arithmetic
+Specification of floating-point arithmetic
Library Stdlib.Floats.SpecFloat
of the Flocq library (see http://flocq.gforge.inria.fr/)
Inductive specification of floating-point numbers
+Inductive specification of floating-point numbers
Library Stdlib.Floats.SpecFloat
Parameterized definitions
+Parameterized definitions
Library Stdlib.Floats.SpecFloat
Library Stdlib.Init.Byte
Library Stdlib.Init.Datatypes
Datatypes with zero and one element
+Datatypes with zero and one element
Library Stdlib.Init.Datatypes
Library Stdlib.Init.Datatypes
Library Stdlib.Init.Datatypes
Misc Other Datatypes
+Misc Other Datatypes
Library Stdlib.Init.Decimal
Decimal numbers
+Decimal numbers
Library Stdlib.Init.Hexadecimal
Hexadecimal numbers
+Hexadecimal numbers
Library Stdlib.Init.Logic
Being inhabited
+Being inhabited
Library Stdlib.Init.Nat
Peano natural numbers, definitions of operations
+Peano natural numbers, definitions of operations
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Conversion with a decimal representation for printing/parsing
+Conversion with a decimal representation for printing/parsing
Library Stdlib.Init.Nat
Library Stdlib.Init.Nat
Log2
+Log2
Library Stdlib.Init.Number
Library Stdlib.Init.Tactics
inversion_sigma
+inversion_sigma
The built-in inversion will frequently leave equalities of
dependent pairs. When the first type in the pair is an hProp or
otherwise simplifies, inversion_sigma is useful; it will replace
diff --git a/master/stdlib/Stdlib.Init.Tauto.html b/master/stdlib/Stdlib.Init.Tauto.html
index d33b4bdf7e..cfa2336e8d 100644
--- a/master/stdlib/Stdlib.Init.Tauto.html
+++ b/master/stdlib/Stdlib.Init.Tauto.html
@@ -49,7 +49,7 @@ Library Stdlib.Init.Tauto
Library Stdlib.Init.Wf
This module proves the validity of
+This module proves the validity of
Library Stdlib.Lists.List
Basics: definition of polymorphic lists and some operations
+Basics: definition of polymorphic lists and some operations
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Applying functions to the elements of a list
+Applying functions to the elements of a list
Map
+Map
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Miscellaneous operations on lists
+Miscellaneous operations on lists
Length order of lists
+Length order of lists
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Combining pairs of lists of possibly-different lengths
+Combining pairs of lists of possibly-different lengths
Library Stdlib.Lists.List
Predicate for List addition/removal (no need for decidability)
+Predicate for List addition/removal (no need for decidability)
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Library Stdlib.Lists.List
Inversion of predicates over lists based on head symbol
+Inversion of predicates over lists based on head symbol
Library Stdlib.Lists.List
Library Stdlib.Lists.SetoidList
Logical relations over lists with respect to a setoid equality
+Logical relations over lists with respect to a setoid equality
or ordering.
Library Stdlib.Lists.StreamMemo
Memoization
+Memoization
Library Stdlib.Logic.ChoiceFacts
References:
+ intuitionistic logic. References:
Library Stdlib.Logic.ChoiceFacts
Constructive choice and description
+Constructive choice and description
Library Stdlib.Logic.ChoiceFacts
Weakly classical choice and description
+Weakly classical choice and description
Library Stdlib.Logic.ChoiceFacts
Table of contents
+Table of contents
Library Stdlib.Logic.ChoiceFacts
AC_rel + AC! = AC_fun
+AC_rel + AC! = AC_fun
Library Stdlib.Logic.ChoiceFacts
Connection between the guarded, non guarded and omniscient choices
+Connection between the guarded, non guarded and omniscient choices
Library Stdlib.Logic.ChoiceFacts
irrelevance)
AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel
+AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel
Library Stdlib.Logic.ChoiceFacts
AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
+AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
Library Stdlib.Logic.ChoiceFacts
D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker
+D_iota -> ID_iota and D_epsilon <-> ID_epsilon + Drinker
Library Stdlib.Logic.ChoiceFacts
Derivability of choice for decidable relations with well-ordered codomain
+Derivability of choice for decidable relations with well-ordered codomain
Library Stdlib.Logic.ChoiceFacts
AC_fun = AC_fun_dep = AC_trunc
+AC_fun = AC_fun_dep = AC_trunc
Choice on dependent and non dependent function types are equivalent
+Choice on dependent and non dependent function types are equivalent
Library Stdlib.Logic.ChoiceFacts
Functional choice and truncation choice are equivalent
+Functional choice and truncation choice are equivalent
Library Stdlib.Logic.ChoiceFacts
Reification of dependent and non dependent functional relation are equivalent
+Reification of dependent and non dependent functional relation are equivalent
Library Stdlib.Logic.ChoiceFacts
Non contradiction of constructive descriptions wrt functional axioms of choice
+Non contradiction of constructive descriptions wrt functional axioms of choice
Non contradiction of indefinite description
+Non contradiction of indefinite description
Library Stdlib.Logic.ChoiceFacts
Library Stdlib.Logic.ChoiceFacts
Excluded-middle + definite description => computational excluded-middle
+Excluded-middle + definite description => computational excluded-middle
Library Stdlib.Logic.ChoiceFacts
Library Stdlib.Logic.ChoiceFacts
Library Stdlib.Logic.ChoiceFacts
Consequences of the choice of a representative in an equivalence class
+Consequences of the choice of a representative in an equivalence class
Library Stdlib.Logic.ChoiceFacts
This is a variant of Diaconescu and Goodman-Myhill theorems
+This is a variant of Diaconescu and Goodman-Myhill theorems
Library Stdlib.Logic.ChoiceFacts
AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple
+AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple
Library Stdlib.Logic.ChoiceFacts
Library Stdlib.Logic.ChoiceFacts
functional forms, SetoidFunctionalChoice seems strictly stronger
AC_fun_setoid = AC_fun + Ext_fun_repr + EM
+AC_fun_setoid = AC_fun + Ext_fun_repr + EM
Library Stdlib.Logic.ChoiceFacts
This is the main theorem in [Carlström04]
+This is the main theorem in [Carlström04]
Library Stdlib.Logic.ChoiceFacts
AC_fun_setoid = AC_fun + Ext_pred_repr + PI
+AC_fun_setoid = AC_fun + Ext_pred_repr + PI
Library Stdlib.Logic.ChoiceFacts
Library Stdlib.Logic.ClassicalEpsilon
Library Stdlib.Logic.ClassicalFacts
Prop degeneracy = excluded-middle + prop extensionality
+Prop degeneracy = excluded-middle + prop extensionality
Library Stdlib.Logic.ClassicalFacts
Classical logic and proof-irrelevance
+Classical logic and proof-irrelevance
CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint
+CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint
Library Stdlib.Logic.ClassicalFacts
CC |- prop_ext /\ dep elim on bool -> proof-irrelevance
+CC |- prop_ext /\ dep elim on bool -> proof-irrelevance
Library Stdlib.Logic.ClassicalFacts
CIC |- prop. ext. -> proof-irrelevance
+CIC |- prop. ext. -> proof-irrelevance
Library Stdlib.Logic.ClassicalFacts
CC |- excluded-middle + dep elim on bool -> proof-irrelevance
+CC |- excluded-middle + dep elim on bool -> proof-irrelevance
Library Stdlib.Logic.ClassicalFacts
CIC |- excluded-middle -> proof-irrelevance
+CIC |- excluded-middle -> proof-irrelevance
Library Stdlib.Logic.ClassicalFacts
Weak classical axioms
+Weak classical axioms
Library Stdlib.Logic.ClassicalFacts
Weak excluded-middle
+Weak excluded-middle
Library Stdlib.Logic.ClassicalFacts
Independence of general premises and drinker's paradox
+Independence of general premises and drinker's paradox
Library Stdlib.Logic.ClassicalFacts
Axioms equivalent to classical logic
+Axioms equivalent to classical logic
Principle of unrestricted minimization
+Principle of unrestricted minimization
Library Stdlib.Logic.ClassicalFacts
Choice of representatives in a partition of bool
+Choice of representatives in a partition of bool
Library Stdlib.Logic.Diaconescu
Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle
+Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle
Library Stdlib.Logic.Diaconescu
Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality
+Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality
Library Stdlib.Logic.Diaconescu
Extensional Hilbert's epsilon description operator -> Excluded-Middle
+Extensional Hilbert's epsilon description operator -> Excluded-Middle
Library Stdlib.Logic.EqdepFacts
Definition of dependent equality and equivalence with equality of dependent pairs
+Definition of dependent equality and equivalence with equality of dependent pairs
Library Stdlib.Logic.EqdepFacts
Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
+Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
Library Stdlib.Logic.EqdepFacts
Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq
+Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq
Library Stdlib.Logic.Eqdep_dec
Streicher's K and injectivity of dependent pair hold on decidable types
+Streicher's K and injectivity of dependent pair hold on decidable types
Library Stdlib.Logic.Eqdep_dec
Definition of the functor that builds properties of dependent equalities on decidable sets in Type
+Definition of the functor that builds properties of dependent equalities on decidable sets in Type
Library Stdlib.Logic.Eqdep_dec
Definition of the functor that builds properties of dependent equalities on decidable sets in Set
+Definition of the functor that builds properties of dependent equalities on decidable sets in Set
Library Stdlib.Logic.ExtensionalityFacts
Functional extensionality <-> Equality of projections from diagonal
+Functional extensionality <-> Equality of projections from diagonal
Library Stdlib.Logic.ExtensionalityFacts
Functional extensionality <-> Unicity of bijection inverse
+Functional extensionality <-> Unicity of bijection inverse
Library Stdlib.Logic.ExtensionalityFacts
Functional extensionality <-> Bijectivity of bijective composition
+Functional extensionality <-> Bijectivity of bijective composition
Library Stdlib.Logic.FinFun
Functions on finite domains
+Functions on finite domains
Library Stdlib.Logic.Hurkens
A modular proof of Hurkens's paradox.
+A modular proof of Hurkens's paradox.
Library Stdlib.Logic.Hurkens
Axiomatisation of impredicative universes in a Martin-Löf style
+Axiomatisation of impredicative universes in a Martin-Löf style
Library Stdlib.Logic.Hurkens
actual system U-.
Large universe
+Large universe
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Impredicative universes are not retracts.
+Impredicative universes are not retracts.
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Modal fragments of Prop are not retracts
+Modal fragments of Prop are not retracts
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Retract of the modal fragment of Prop in a small type
+Retract of the modal fragment of Prop in a small type
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
The negative fragment of Prop is not a retract
+The negative fragment of Prop is not a retract
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Retract of the negative fragment of Prop in a small type
+Retract of the negative fragment of Prop in a small type
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Retract of Prop in a small type, using the identity modality.
+Retract of Prop in a small type, using the identity modality.
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Retract of Prop in a small type
+Retract of Prop in a small type
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Large universes are not retracts of Prop.
+Large universes are not retracts of Prop.
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Library Stdlib.Logic.Hurkens
Universe U is a retract of A
+Universe U is a retract of A
Library Stdlib.Logic.Hurkens
Prop<>Type.
+Prop<>Type.
Library Stdlib.Logic.PropExtensionalityFacts
Propositional and predicate extensionality
+Propositional and predicate extensionality
Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality
+Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality
Library Stdlib.Logic.PropExtensionalityFacts
Propositional extensionality and provable proposition extensionality
+Propositional extensionality and provable proposition extensionality
Library Stdlib.Logic.PropExtensionalityFacts
Propositional extensionality and refutable proposition extensionality
+Propositional extensionality and refutable proposition extensionality
Library Stdlib.Logic.PropFacts
Basic facts about Prop as a type
+Basic facts about Prop as a type
Library Stdlib.Logic.SetIsType
The Set universe seen as a synonym for Type
+The Set universe seen as a synonym for Type
Library Stdlib.MSets.MSetAVL
MSetAVL : Implementation of MSetInterface via AVL trees
+MSetAVL : Implementation of MSetInterface via AVL trees
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Generic trees instantiated with integer height
+Generic trees instantiated with integer height
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Extraction of minimum element
+Extraction of minimum element
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Library Stdlib.MSets.MSetAVL
Encapsulation
+Encapsulation
Library Stdlib.MSets.MSetDecide
Overview
+Overview
This functor defines the tactic fsetdec, which will
solve any valid goal of the form
@@ -181,7 +181,7 @@ Library Stdlib.MSets.MSetDecide
Facts and Tactics for Propositional Logic
+Facts and Tactics for Propositional Logic
These lemmas and tactics are in a module so that they do
not affect the namespace if you import the enclosing
@@ -196,18 +196,18 @@ Library Stdlib.MSets.MSetDecide
Lemmas and Tactics About Decidable Propositions
+Lemmas and Tactics About Decidable Propositions
Propositional Equivalences Involving Negation
+Propositional Equivalences Involving Negation
These are all written with the unfolded form of
negation, since I am not sure if setoid rewriting will
always perform conversion.
Tactics for Negations
+Tactics for Negations
Library Stdlib.MSets.MSetDecide
Auxiliary Tactics
+Auxiliary Tactics
Again, these lemmas and tactics are in a module so that
they do not affect the namespace if you import the
@@ -471,7 +471,7 @@ Library Stdlib.MSets.MSetDecide
Generic Tactics
+Generic Tactics
We begin by defining a few generic, useful tactics.
Library Stdlib.MSets.MSetDecide
Discarding Irrelevant Hypotheses
+Discarding Irrelevant Hypotheses
We will want to clear the context of any
non-MSet-related hypotheses in order to increase the
@@ -668,7 +668,7 @@ Library Stdlib.MSets.MSetDecide
Turning Set Operators into Propositional Connectives
+Turning Set Operators into Propositional Connectives
The lemmas from MSetFacts will be used to break down
set operations into propositional formulas built over
@@ -694,7 +694,7 @@ Library Stdlib.MSets.MSetDecide
Decidability of MSet Propositions
+Decidability of MSet Propositions
Library Stdlib.MSets.MSetDecide
Normalizing Propositions About Equality
+Normalizing Propositions About Equality
We have to deal with the fact that E.eq may be
convertible with Coq's equality. Thus, we will find the
@@ -812,7 +812,7 @@ Library Stdlib.MSets.MSetDecide
Considering Decidability of Base Propositions
+Considering Decidability of Base Propositions
This tactic adds assertions about the decidability of
E.eq and In to the context. This is necessary for
@@ -861,7 +861,7 @@ Library Stdlib.MSets.MSetDecide
Handling Empty, Subset, and Equal
+Handling Empty, Subset, and Equal
This tactic instantiates universally quantified
hypotheses (which arise from the unfolding of Empty,
@@ -909,7 +909,7 @@ Library Stdlib.MSets.MSetDecide
The Core fsetdec Auxiliary Tactics
+The Core fsetdec Auxiliary Tactics
Library Stdlib.MSets.MSetDecide
The fsetdec Tactic
+The fsetdec Tactic
Here is the top-level tactic (the only one intended for
clients of this library). It's specification is given at
@@ -1065,7 +1065,7 @@ Library Stdlib.MSets.MSetDecide
Library Stdlib.MSets.MSetEqProperties
Finite sets library
+Finite sets library
Library Stdlib.MSets.MSetFacts
Specifications written using implications :
+Specifications written using implications :
this used to be the default interface.
Library Stdlib.MSets.MSetFacts
Specifications written using equivalences :
+Specifications written using equivalences :
this is now provided by the default interface.
Library Stdlib.MSets.MSetFacts
Library Stdlib.MSets.MSetFacts
Declarations of morphisms with respects to E.eq and Equal
+Declarations of morphisms with respects to E.eq and Equal
Library Stdlib.MSets.MSetGenTree
MSetGenTree : sets via generic trees
+MSetGenTree : sets via generic trees
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Testing universal or existential properties.
+Testing universal or existential properties.
Library Stdlib.MSets.MSetGenTree
Props : correctness proofs of these generic operations
+Props : correctness proofs of these generic operations
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetGenTree
Library Stdlib.MSets.MSetInterface
Functorial signature for weak sets
+Functorial signature for weak sets
Library Stdlib.MSets.MSetInterface
Static signature for weak sets
+Static signature for weak sets
Library Stdlib.MSets.MSetInterface
Functorial signature for sets on ordered elements
+Functorial signature for sets on ordered elements
Library Stdlib.MSets.MSetInterface
Static signature for sets on ordered elements
+Static signature for sets on ordered elements
Library Stdlib.MSets.MSetInterface
Some subtyping tests
+Some subtyping tests
WSetsOn ---> WSets
@@ -604,7 +604,7 @@
Library Stdlib.MSets.MSetInterface
Signatures for set representations with ill-formed values.
+Signatures for set representations with ill-formed values.
Library Stdlib.MSets.MSetList
Library Stdlib.MSets.MSetList
Library Stdlib.MSets.MSetList
Encapsulation
+Encapsulation
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Induction principles for fold (contributed by S. Lescuyer)
+Induction principles for fold (contributed by S. Lescuyer)
Library Stdlib.MSets.MSetProperties
Alternative (weaker) specifications for fold
+Alternative (weaker) specifications for fold
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Cardinal
+Cardinal
Characterization of cardinal in terms of fold
+Characterization of cardinal in terms of fold
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetProperties
Library Stdlib.MSets.MSetRBT
MSetRBT : Implementation of MSetInterface via Red-Black trees
+MSetRBT : Implementation of MSetInterface via Red-Black trees
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Generic trees instantiated with color
+Generic trees instantiated with color
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Union, intersection, difference
+Union, intersection, difference
Library Stdlib.MSets.MSetRBT
MakeRaw : the pure functions and their specifications
+MakeRaw : the pure functions and their specifications
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Generic handling for red-matching and red-red-matching
+Generic handling for red-matching and red-red-matching
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
An invariant for binary list functions with accumulator.
+An invariant for binary list functions with accumulator.
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Library Stdlib.MSets.MSetRBT
Final Encapsulation
+Final Encapsulation
Library Stdlib.MSets.MSetToFiniteSet
Finite sets library : conversion to old Finite_sets
+Finite sets library : conversion to old Finite_sets
Library Stdlib.MSets.MSetToFiniteSet
Going from MSets with usual Leibniz equality
+Going from MSets with usual Leibniz equality
to the good old Ensembles and Finite_sets theory.
Library Stdlib.MSets.MSetWeakList