From d550adc90941659a76127fe1723699ce52cb251c Mon Sep 17 00:00:00 2001 From: coqbot Date: Mon, 24 Feb 2025 15:56:23 +0000 Subject: [PATCH] =?UTF-8?q?Documentation=20of=20branch=20=E2=80=9Cmaster?= =?UTF-8?q?=E2=80=9D=20at=20a7dca42e?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- master/corelib/Corelib.BinNums.IntDef.html | 34 ++++++------- master/corelib/Corelib.BinNums.NatDef.html | 8 +-- master/corelib/Corelib.BinNums.PosDef.html | 40 +++++++-------- .../corelib/Corelib.Classes.CMorphisms.html | 4 +- .../Corelib.Classes.CRelationClasses.html | 6 +-- .../corelib/Corelib.Classes.Equivalence.html | 2 +- master/corelib/Corelib.Classes.Init.html | 2 +- master/corelib/Corelib.Classes.Morphisms.html | 4 +- .../Corelib.Classes.Morphisms_Prop.html | 2 +- .../Corelib.Classes.RelationClasses.html | 6 +-- .../Corelib.Classes.SetoidTactics.html | 2 +- .../corelib/Corelib.Floats.FloatAxioms.html | 2 +- master/corelib/Corelib.Floats.FloatOps.html | 2 +- master/corelib/Corelib.Floats.PrimFloat.html | 22 ++++----- master/corelib/Corelib.Floats.SpecFloat.html | 8 +-- master/corelib/Corelib.Init.Byte.html | 2 +- master/corelib/Corelib.Init.Datatypes.html | 14 +++--- master/corelib/Corelib.Init.Decimal.html | 2 +- master/corelib/Corelib.Init.Hexadecimal.html | 2 +- master/corelib/Corelib.Init.Logic.html | 8 +-- master/corelib/Corelib.Init.Nat.html | 28 +++++------ master/corelib/Corelib.Init.Number.html | 2 +- master/corelib/Corelib.Init.Tactics.html | 4 +- master/corelib/Corelib.Init.Tauto.html | 2 +- master/corelib/Corelib.Init.Wf.html | 2 +- master/corelib/Corelib.Lists.ListDef.html | 10 ++-- .../Corelib.Strings.PrimStringAxioms.html | 4 +- master/corelib/index_global_T.html | 2 +- master/corelib/index_global_W.html | 2 +- master/corelib/index_library_T.html | 2 +- master/corelib/index_library_W.html | 2 +- .../.doctrees/environment.pickle | Bin 68955 -> 68955 bytes .../.doctrees/language/coq-library.doctree | Bin 231140 -> 231140 bytes .../.doctrees/addendum/extraction.doctree | Bin 355371 -> 355371 bytes .../addendum/generalized-rewriting.doctree | Bin 866882 -> 866882 bytes .../addendum/implicit-coercions.doctree | Bin 481483 -> 481483 bytes .../.doctrees/addendum/micromega.doctree | Bin 398220 -> 398220 bytes .../addendum/miscellaneous-extensions.doctree | Bin 100914 -> 100914 bytes .../refman/.doctrees/addendum/program.doctree | Bin 247075 -> 247075 bytes .../.doctrees/addendum/rewrite-rules.doctree | Bin 169832 -> 169832 bytes master/refman/.doctrees/addendum/ring.doctree | Bin 684756 -> 684756 bytes .../refman/.doctrees/addendum/sprop.doctree | Bin 355727 -> 355727 bytes .../.doctrees/addendum/type-classes.doctree | Bin 519689 -> 519689 bytes .../addendum/universe-polymorphism.doctree | Bin 951343 -> 951343 bytes master/refman/.doctrees/changes.doctree | Bin 4645479 -> 4645479 bytes master/refman/.doctrees/environment.pickle | Bin 856151 -> 856151 bytes master/refman/.doctrees/language/cic.doctree | Bin 143381 -> 143381 bytes .../.doctrees/language/coq-library.doctree | Bin 930322 -> 930322 bytes .../language/core/assumptions.doctree | Bin 187048 -> 187048 bytes .../.doctrees/language/core/basic.doctree | Bin 368763 -> 368763 bytes .../language/core/coinductive.doctree | Bin 195717 -> 195717 bytes .../language/core/conversion.doctree | Bin 123537 -> 123537 bytes .../.doctrees/language/core/inductive.doctree | Bin 1245522 -> 1245522 bytes .../.doctrees/language/core/modules.doctree | Bin 650160 -> 650160 bytes .../.doctrees/language/core/primitive.doctree | Bin 166504 -> 166504 bytes .../.doctrees/language/core/records.doctree | Bin 432432 -> 432432 bytes .../.doctrees/language/core/sections.doctree | Bin 171542 -> 171542 bytes .../.doctrees/language/core/variants.doctree | Bin 344119 -> 344119 bytes .../extensions/arguments-command.doctree | Bin 552388 -> 552388 bytes .../language/extensions/canonical.doctree | Bin 881842 -> 881842 bytes .../language/extensions/evars.doctree | Bin 205100 -> 205100 bytes .../extensions/implicit-arguments.doctree | Bin 548969 -> 548969 bytes .../language/extensions/match.doctree | Bin 977532 -> 977532 bytes .../practical-tools/coq-commands.doctree | Bin 236413 -> 236413 bytes .../.doctrees/practical-tools/coqide.doctree | Bin 200551 -> 200551 bytes .../.doctrees/proof-engine/ltac.doctree | Bin 2090856 -> 2090856 bytes .../.doctrees/proof-engine/ltac2.doctree | Bin 1287808 -> 1287808 bytes .../ssreflect-proof-language.doctree | Bin 5550930 -> 5550930 bytes .../.doctrees/proof-engine/tactics.doctree | Bin 1587240 -> 1587240 bytes .../proof-engine/vernacular-commands.doctree | Bin 846588 -> 846588 bytes .../proofs/automatic-tactics/auto.doctree | Bin 567995 -> 567995 bytes .../proofs/automatic-tactics/logic.doctree | Bin 215606 -> 215606 bytes .../proofs/writing-proofs/equality.doctree | Bin 890102 -> 890111 bytes .../proofs/writing-proofs/proof-mode.doctree | Bin 703750 -> 703750 bytes .../reasoning-inductives.doctree | Bin 1729018 -> 1729018 bytes .../user-extensions/syntax-extensions.doctree | Bin 2222760 -> 2222760 bytes .../.doctrees/using/libraries/funind.doctree | Bin 425149 -> 425149 bytes .../.doctrees/using/libraries/writing.doctree | Bin 123480 -> 123480 bytes master/refman/proof-engine/ltac.html | 46 +++++++++--------- .../proofs/writing-proofs/equality.html | 8 +-- master/refman/searchindex.js | 2 +- 81 files changed, 144 insertions(+), 144 deletions(-) diff --git a/master/corelib/Corelib.BinNums.IntDef.html b/master/corelib/Corelib.BinNums.IntDef.html index 2054205c03..8eff73e605 100644 --- a/master/corelib/Corelib.BinNums.IntDef.html +++ b/master/corelib/Corelib.BinNums.IntDef.html @@ -276,7 +276,7 @@

Library Corelib.BinNums.IntDef

-

Binary Integers, Definitions of Operations

+

Binary Integers, Definitions of Operations

@@ -291,7 +291,7 @@

Library Corelib.BinNums.IntDef

-

Doubling and variants

+

Doubling and variants

@@ -324,7 +324,7 @@

Library Corelib.BinNums.IntDef

-

Subtraction of positive into Z

+

Subtraction of positive into Z

@@ -347,7 +347,7 @@

Library Corelib.BinNums.IntDef

-

Addition

+

Addition

@@ -370,7 +370,7 @@

Library Corelib.BinNums.IntDef

-

Opposite

+

Opposite

@@ -390,7 +390,7 @@

Library Corelib.BinNums.IntDef

-

Subtraction

+

Subtraction

@@ -405,7 +405,7 @@

Library Corelib.BinNums.IntDef

-

Multiplication

+

Multiplication

@@ -428,7 +428,7 @@

Library Corelib.BinNums.IntDef

-

Power function

+

Power function

@@ -451,7 +451,7 @@

Library Corelib.BinNums.IntDef

-

Comparison

+

Comparison

@@ -520,7 +520,7 @@

Library Corelib.BinNums.IntDef

-

Minimum and maximum

+

Minimum and maximum

@@ -543,7 +543,7 @@

Library Corelib.BinNums.IntDef

-

Conversions

+

Conversions

@@ -607,11 +607,11 @@

Library Corelib.BinNums.IntDef

-

Euclidean divisions for binary integers

+

Euclidean divisions for binary integers

-

Floor division

+

Floor division

@@ -702,7 +702,7 @@

Library Corelib.BinNums.IntDef

-

Trunc Division

+

Trunc Division

@@ -763,7 +763,7 @@

Library Corelib.BinNums.IntDef

No infix notation for rem, otherwise it becomes a keyword
-

Parity functions

+

Parity functions

@@ -781,7 +781,7 @@

Library Corelib.BinNums.IntDef

-

Division by two

+

Division by two

@@ -804,7 +804,7 @@

Library Corelib.BinNums.IntDef

-

Square root

+

Square root

diff --git a/master/corelib/Corelib.BinNums.NatDef.html b/master/corelib/Corelib.BinNums.NatDef.html index 232d2efc26..87811ec9ee 100644 --- a/master/corelib/Corelib.BinNums.NatDef.html +++ b/master/corelib/Corelib.BinNums.NatDef.html @@ -270,7 +270,7 @@

Library Corelib.BinNums.NatDef

-

Binary natural numbers, definitions of operations

+

Binary natural numbers, definitions of operations

@@ -282,7 +282,7 @@

Library Corelib.BinNums.NatDef

-

Operation x -> 2*x+1

+

Operation x -> 2*x+1

@@ -298,7 +298,7 @@

Library Corelib.BinNums.NatDef

-

Operation x -> 2*x

+

Operation x -> 2*x

@@ -314,7 +314,7 @@

Library Corelib.BinNums.NatDef

-

The successor of a N can be seen as a positive

+

The successor of a N can be seen as a positive

diff --git a/master/corelib/Corelib.BinNums.PosDef.html b/master/corelib/Corelib.BinNums.PosDef.html index 07c2af74e0..23471499c2 100644 --- a/master/corelib/Corelib.BinNums.PosDef.html +++ b/master/corelib/Corelib.BinNums.PosDef.html @@ -267,7 +267,7 @@

Library Corelib.BinNums.PosDef

-

Binary positive numbers, operations

+

Binary positive numbers, operations

@@ -315,11 +315,11 @@

Library Corelib.BinNums.PosDef

-

Operations over positive numbers

+

Operations over positive numbers

-

Successor

+

Successor

@@ -336,7 +336,7 @@

Library Corelib.BinNums.PosDef

-

Addition

+

Addition

@@ -372,7 +372,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x-1

+

Operation x -> 2*x-1

@@ -389,7 +389,7 @@

Library Corelib.BinNums.PosDef

-

The predecessor of a positive number can be seen as a N

+

The predecessor of a positive number can be seen as a N

@@ -406,7 +406,7 @@

Library Corelib.BinNums.PosDef

-

An auxiliary type for subtraction

+

An auxiliary type for subtraction

@@ -421,7 +421,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x+1

+

Operation x -> 2*x+1

@@ -438,7 +438,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x

+

Operation x -> 2*x

@@ -455,7 +455,7 @@

Library Corelib.BinNums.PosDef

-

Operation x -> 2*x-2

+

Operation x -> 2*x-2

@@ -472,7 +472,7 @@

Library Corelib.BinNums.PosDef

-

Subtraction, result as a mask

+

Subtraction, result as a mask

@@ -505,7 +505,7 @@

Library Corelib.BinNums.PosDef

-

Subtraction, result as a positive, returning 1 if x<=y

+

Subtraction, result as a positive, returning 1 if x<=y

@@ -521,7 +521,7 @@

Library Corelib.BinNums.PosDef

-

Multiplication

+

Multiplication

@@ -538,7 +538,7 @@

Library Corelib.BinNums.PosDef

-

Iteration over a positive number

+

Iteration over a positive number

@@ -555,7 +555,7 @@

Library Corelib.BinNums.PosDef

-

Division by 2 rounded below but for 1

+

Division by 2 rounded below but for 1

@@ -588,7 +588,7 @@

Library Corelib.BinNums.PosDef

-

Comparison on binary positive numbers

+

Comparison on binary positive numbers

@@ -614,7 +614,7 @@

Library Corelib.BinNums.PosDef

-

Boolean equality and comparisons

+

Boolean equality and comparisons

@@ -636,7 +636,7 @@

Library Corelib.BinNums.PosDef

-

A Square Root function for positive numbers

+

A Square Root function for positive numbers

@@ -784,7 +784,7 @@

Library Corelib.BinNums.PosDef

-

From binary positive numbers to Peano natural numbers

+

From binary positive numbers to Peano natural numbers

@@ -806,7 +806,7 @@

Library Corelib.BinNums.PosDef

-

From Peano natural numbers to binary positive numbers

+

From Peano natural numbers to binary positive numbers

diff --git a/master/corelib/Corelib.Classes.CMorphisms.html b/master/corelib/Corelib.Classes.CMorphisms.html index 9ac05a3254..07616dd93a 100644 --- a/master/corelib/Corelib.Classes.CMorphisms.html +++ b/master/corelib/Corelib.Classes.CMorphisms.html @@ -267,7 +267,7 @@

Library Corelib.Classes.CMorphisms

-

Typeclass-based morphism definition and standard, minimal instances

+

Typeclass-based morphism definition and standard, minimal instances

@@ -296,7 +296,7 @@

Library Corelib.Classes.CMorphisms

-

Morphisms.

+

Morphisms.

diff --git a/master/corelib/Corelib.Classes.CRelationClasses.html b/master/corelib/Corelib.Classes.CRelationClasses.html index 45a87b8bb8..72d870afc5 100644 --- a/master/corelib/Corelib.Classes.CRelationClasses.html +++ b/master/corelib/Corelib.Classes.CRelationClasses.html @@ -267,7 +267,7 @@

Library Corelib.Classes.CRelationClasses

-

Typeclass-based relations, tactics and standard instances

+

Typeclass-based relations, tactics and standard instances

@@ -672,7 +672,7 @@

Library Corelib.Classes.CRelationClasses

We can already dualize all these properties.
-

Standard instances.

+

Standard instances.

@@ -825,7 +825,7 @@

Library Corelib.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/corelib/Corelib.Classes.Equivalence.html b/master/corelib/Corelib.Classes.Equivalence.html index cbc6a5fd48..53ad8e09db 100644 --- a/master/corelib/Corelib.Classes.Equivalence.html +++ b/master/corelib/Corelib.Classes.Equivalence.html @@ -267,7 +267,7 @@

Library Corelib.Classes.Equivalence

-

Typeclass-based setoids. Definitions on Equivalence.

+

Typeclass-based setoids. Definitions on Equivalence.

diff --git a/master/corelib/Corelib.Classes.Init.html b/master/corelib/Corelib.Classes.Init.html index b153ec7b8c..26f377bd1a 100644 --- a/master/corelib/Corelib.Classes.Init.html +++ b/master/corelib/Corelib.Classes.Init.html @@ -267,7 +267,7 @@

Library Corelib.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/corelib/Corelib.Classes.Morphisms.html b/master/corelib/Corelib.Classes.Morphisms.html index db8fc44518..9064643d89 100644 --- a/master/corelib/Corelib.Classes.Morphisms.html +++ b/master/corelib/Corelib.Classes.Morphisms.html @@ -267,7 +267,7 @@

Library Corelib.Classes.Morphisms

-

Typeclass-based morphism definition and standard, minimal instances

+

Typeclass-based morphism definition and standard, minimal instances

@@ -292,7 +292,7 @@

Library Corelib.Classes.Morphisms

-

Morphisms.

+

Morphisms.

diff --git a/master/corelib/Corelib.Classes.Morphisms_Prop.html b/master/corelib/Corelib.Classes.Morphisms_Prop.html index 6f50c633cd..f6a6394548 100644 --- a/master/corelib/Corelib.Classes.Morphisms_Prop.html +++ b/master/corelib/Corelib.Classes.Morphisms_Prop.html @@ -267,7 +267,7 @@

Library Corelib.Classes.Morphisms_Prop

-

Proper instances for propositional connectives.

+

Proper instances for propositional connectives.

diff --git a/master/corelib/Corelib.Classes.RelationClasses.html b/master/corelib/Corelib.Classes.RelationClasses.html index d31fd6e0fa..f1632ffc64 100644 --- a/master/corelib/Corelib.Classes.RelationClasses.html +++ b/master/corelib/Corelib.Classes.RelationClasses.html @@ -267,7 +267,7 @@

Library Corelib.Classes.RelationClasses

-

Typeclass-based relations, tactics and standard instances

+

Typeclass-based relations, tactics and standard instances

@@ -698,7 +698,7 @@

Library Corelib.Classes.RelationClasses

We can already dualize all these properties.
-

Standard instances.

+

Standard instances.

@@ -1065,7 +1065,7 @@

Library Corelib.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/corelib/Corelib.Classes.SetoidTactics.html b/master/corelib/Corelib.Classes.SetoidTactics.html index 528e1fb0e1..6229bdc16a 100644 --- a/master/corelib/Corelib.Classes.SetoidTactics.html +++ b/master/corelib/Corelib.Classes.SetoidTactics.html @@ -267,7 +267,7 @@

Library Corelib.Classes.SetoidTactics

-

Tactics for typeclass-based setoids.

+

Tactics for typeclass-based setoids.

diff --git a/master/corelib/Corelib.Floats.FloatAxioms.html b/master/corelib/Corelib.Floats.FloatAxioms.html index 17bd50a8e9..09fc5c6291 100644 --- a/master/corelib/Corelib.Floats.FloatAxioms.html +++ b/master/corelib/Corelib.Floats.FloatAxioms.html @@ -271,7 +271,7 @@

Library Corelib.Floats.FloatAxioms

-

Properties of the primitive operators for the Binary64 format

+

Properties of the primitive operators for the Binary64 format

diff --git a/master/corelib/Corelib.Floats.FloatOps.html b/master/corelib/Corelib.Floats.FloatOps.html index 518d4c4095..e459c2996a 100644 --- a/master/corelib/Corelib.Floats.FloatOps.html +++ b/master/corelib/Corelib.Floats.FloatOps.html @@ -271,7 +271,7 @@

Library Corelib.Floats.FloatOps

-

Derived operations and mapping between primitive floats and spec_floats

+

Derived operations and mapping between primitive floats and spec_floats

diff --git a/master/corelib/Corelib.Floats.PrimFloat.html b/master/corelib/Corelib.Floats.PrimFloat.html index a863f807d7..528026adb1 100644 --- a/master/corelib/Corelib.Floats.PrimFloat.html +++ b/master/corelib/Corelib.Floats.PrimFloat.html @@ -270,7 +270,7 @@

Library Corelib.Floats.PrimFloat

-

Definition of the interface for primitive floating-point arithmetic

+

Definition of the interface for primitive floating-point arithmetic

@@ -279,7 +279,7 @@

Library Corelib.Floats.PrimFloat

IEEE 754-2008 standard.
-

Type definition for the co-domain of compare

+

Type definition for the co-domain of compare

@@ -295,7 +295,7 @@

Library Corelib.Floats.PrimFloat

-

The main type

+

The main type

float: primitive type for Binary64 floating-point numbers.
@@ -313,7 +313,7 @@

Library Corelib.Floats.PrimFloat

-

Syntax support

+

Syntax support

@@ -328,7 +328,7 @@

Library Corelib.Floats.PrimFloat

-

Floating-point operators

+

Floating-point operators

@@ -403,7 +403,7 @@

Library Corelib.Floats.PrimFloat

-

Conversions

+

Conversions

@@ -442,7 +442,7 @@

Library Corelib.Floats.PrimFloat

-

Exponent manipulation functions

+

Exponent manipulation functions

frshiftexp: convert a float to fractional part in [0.5, 1.) and integer part.
@@ -462,7 +462,7 @@

Library Corelib.Floats.PrimFloat

-

Predecesor/Successor functions

+

Predecesor/Successor functions

@@ -484,7 +484,7 @@

Library Corelib.Floats.PrimFloat

-

Special values (needed for pretty-printing)

+

Special values (needed for pretty-printing)

@@ -501,7 +501,7 @@

Library Corelib.Floats.PrimFloat

-

Other special values

+

Other special values

@@ -514,7 +514,7 @@

Library Corelib.Floats.PrimFloat

-

Predicates and helper functions

+

Predicates and helper functions

diff --git a/master/corelib/Corelib.Floats.SpecFloat.html b/master/corelib/Corelib.Floats.SpecFloat.html index 1ca185b176..4c7b619528 100644 --- a/master/corelib/Corelib.Floats.SpecFloat.html +++ b/master/corelib/Corelib.Floats.SpecFloat.html @@ -270,7 +270,7 @@

Library Corelib.Floats.SpecFloat

-

Specification of floating-point arithmetic

+

Specification of floating-point arithmetic

@@ -279,7 +279,7 @@

Library Corelib.Floats.SpecFloat

of the Flocq library (see http://flocq.gforge.inria.fr/)
-

Inductive specification of floating-point numbers

+

Inductive specification of floating-point numbers

@@ -297,7 +297,7 @@

Library Corelib.Floats.SpecFloat

-

Parameterized definitions

+

Parameterized definitions

@@ -460,7 +460,7 @@

Library Corelib.Floats.SpecFloat

-

Define operations

+

Define operations

diff --git a/master/corelib/Corelib.Init.Byte.html b/master/corelib/Corelib.Init.Byte.html index f9379bb6ee..773ae69a27 100644 --- a/master/corelib/Corelib.Init.Byte.html +++ b/master/corelib/Corelib.Init.Byte.html @@ -267,7 +267,7 @@

Library Corelib.Init.Byte

-

Bytes

+

Bytes

diff --git a/master/corelib/Corelib.Init.Datatypes.html b/master/corelib/Corelib.Init.Datatypes.html index 5ac4a0e1ba..1c77c946e4 100644 --- a/master/corelib/Corelib.Init.Datatypes.html +++ b/master/corelib/Corelib.Init.Datatypes.html @@ -275,7 +275,7 @@

Library Corelib.Init.Datatypes

-

Datatypes with zero and one element

+

Datatypes with zero and one element

@@ -309,7 +309,7 @@

Library Corelib.Init.Datatypes

-

The boolean datatype

+

The boolean datatype

@@ -339,7 +339,7 @@

Library Corelib.Init.Datatypes

-

Reflect: a specialized inductive type for

+

Reflect: a specialized inductive type for

relating propositions and booleans, as popularized by the Ssreflect library. @@ -505,7 +505,7 @@

Library Corelib.Init.Datatypes

-

Peano natural numbers

+

Peano natural numbers

@@ -540,7 +540,7 @@

Library Corelib.Init.Datatypes

-

Container datatypes

+

Container datatypes

@@ -745,7 +745,7 @@

Library Corelib.Init.Datatypes

-

The comparison datatype

+

The comparison datatype

@@ -863,7 +863,7 @@

Library Corelib.Init.Datatypes

-

Misc Other Datatypes

+

Misc Other Datatypes

diff --git a/master/corelib/Corelib.Init.Decimal.html b/master/corelib/Corelib.Init.Decimal.html index 526bfe4487..b127b0f08d 100644 --- a/master/corelib/Corelib.Init.Decimal.html +++ b/master/corelib/Corelib.Init.Decimal.html @@ -267,7 +267,7 @@

Library Corelib.Init.Decimal

-

Decimal numbers

+

Decimal numbers

diff --git a/master/corelib/Corelib.Init.Hexadecimal.html b/master/corelib/Corelib.Init.Hexadecimal.html index ccce0a96f3..e01bce63ea 100644 --- a/master/corelib/Corelib.Init.Hexadecimal.html +++ b/master/corelib/Corelib.Init.Hexadecimal.html @@ -267,7 +267,7 @@

Library Corelib.Init.Hexadecimal

-

Hexadecimal numbers

+

Hexadecimal numbers

diff --git a/master/corelib/Corelib.Init.Logic.html b/master/corelib/Corelib.Init.Logic.html index ccaee2f8d6..e402818912 100644 --- a/master/corelib/Corelib.Init.Logic.html +++ b/master/corelib/Corelib.Init.Logic.html @@ -277,7 +277,7 @@

Library Corelib.Init.Logic

-

Propositional connectives

+

Propositional connectives

@@ -532,7 +532,7 @@

Library Corelib.Init.Logic

-

First-order quantifiers

+

First-order quantifiers

@@ -685,7 +685,7 @@

Library Corelib.Init.Logic

-

Equality

+

Equality

@@ -1085,7 +1085,7 @@

Library Corelib.Init.Logic

-

Being inhabited

+

Being inhabited

diff --git a/master/corelib/Corelib.Init.Nat.html b/master/corelib/Corelib.Init.Nat.html index 9e784cd61b..9550c19ce4 100644 --- a/master/corelib/Corelib.Init.Nat.html +++ b/master/corelib/Corelib.Init.Nat.html @@ -272,7 +272,7 @@

Library Corelib.Init.Nat

-

Peano natural numbers, definitions of operations

+

Peano natural numbers, definitions of operations

@@ -289,7 +289,7 @@

Library Corelib.Init.Nat

-

Constants

+

Constants

@@ -308,7 +308,7 @@

Library Corelib.Init.Nat

-

Basic operations

+

Basic operations

@@ -377,7 +377,7 @@

Library Corelib.Init.Nat

-

Comparisons

+

Comparisons

@@ -423,7 +423,7 @@

Library Corelib.Init.Nat

-

Minimum, maximum

+

Minimum, maximum

@@ -448,7 +448,7 @@

Library Corelib.Init.Nat

-

Parity tests

+

Parity tests

@@ -468,7 +468,7 @@

Library Corelib.Init.Nat

-

Power

+

Power

@@ -486,7 +486,7 @@

Library Corelib.Init.Nat

-

Tail-recursive versions of add and mul

+

Tail-recursive versions of add and mul

@@ -520,7 +520,7 @@

Library Corelib.Init.Nat

-

Conversion with a decimal representation for printing/parsing

+

Conversion with a decimal representation for printing/parsing

@@ -644,7 +644,7 @@

Library Corelib.Init.Nat

-

Euclidean division

+

Euclidean division

@@ -687,7 +687,7 @@

Library Corelib.Init.Nat

-

Greatest common divisor

+

Greatest common divisor

@@ -709,7 +709,7 @@

Library Corelib.Init.Nat

-

Square

+

Square

@@ -721,7 +721,7 @@

Library Corelib.Init.Nat

-

Square root

+

Square root

@@ -759,7 +759,7 @@

Library Corelib.Init.Nat

-

Log2

+

Log2

diff --git a/master/corelib/Corelib.Init.Number.html b/master/corelib/Corelib.Init.Number.html index 942cfc28c3..3c27b6765e 100644 --- a/master/corelib/Corelib.Init.Number.html +++ b/master/corelib/Corelib.Init.Number.html @@ -267,7 +267,7 @@

Library Corelib.Init.Number

-

Decimal or Hexadecimal numbers

+

Decimal or Hexadecimal numbers

diff --git a/master/corelib/Corelib.Init.Tactics.html b/master/corelib/Corelib.Init.Tactics.html index 44e83fd230..7c365bc394 100644 --- a/master/corelib/Corelib.Init.Tactics.html +++ b/master/corelib/Corelib.Init.Tactics.html @@ -273,7 +273,7 @@

Library Corelib.Init.Tactics

-

Useful tactics

+

Useful tactics

@@ -594,7 +594,7 @@

Library Corelib.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/corelib/Corelib.Init.Tauto.html b/master/corelib/Corelib.Init.Tauto.html index 285af507e7..b3755fde80 100644 --- a/master/corelib/Corelib.Init.Tauto.html +++ b/master/corelib/Corelib.Init.Tauto.html @@ -267,7 +267,7 @@

Library Corelib.Init.Tauto

-

The tauto and intuition tactics

+

The tauto and intuition tactics

diff --git a/master/corelib/Corelib.Init.Wf.html b/master/corelib/Corelib.Init.Wf.html index df026b2c25..06d5ae55c2 100644 --- a/master/corelib/Corelib.Init.Wf.html +++ b/master/corelib/Corelib.Init.Wf.html @@ -267,7 +267,7 @@

Library Corelib.Init.Wf

-

This module proves the validity of

+

This module proves the validity of

-

Basics: definition of polymorphic lists and some operations

+

Basics: definition of polymorphic lists and some operations

@@ -283,7 +283,7 @@

Library Corelib.Lists.ListDef

-

Map

+

Map

@@ -351,7 +351,7 @@

Library Corelib.Lists.ListDef

-

Nth element of a list

+

Nth element of a list

@@ -404,7 +404,7 @@

Library Corelib.Lists.ListDef

-

Existential and universal predicates over lists

+

Existential and universal predicates over lists

@@ -433,7 +433,7 @@

Library Corelib.Lists.ListDef

-

List comparison

+

List comparison

diff --git a/master/corelib/Corelib.Strings.PrimStringAxioms.html b/master/corelib/Corelib.Strings.PrimStringAxioms.html index 6db6bbd201..2d1a03a10a 100644 --- a/master/corelib/Corelib.Strings.PrimStringAxioms.html +++ b/master/corelib/Corelib.Strings.PrimStringAxioms.html @@ -274,7 +274,7 @@

Library Corelib.Strings.PrimStringAxioms

-

Conversion to / from lists

+

Conversion to / from lists

@@ -313,7 +313,7 @@

Library Corelib.Strings.PrimStringAxioms

-

Axioms relating string operations with list operations

+

Axioms relating string operations with list operations

diff --git a/master/corelib/index_global_T.html b/master/corelib/index_global_T.html index 474c8d6888..9735b2585f 100644 --- a/master/corelib/index_global_T.html +++ b/master/corelib/index_global_T.html @@ -743,8 +743,8 @@

T

t [definition, in Corelib.Init.Nat]
-Tactics [library]
Tactics [library]
+Tactics [library]
tactic_view [constructor, in Corelib.ssr.ssreflect]
tag [definition, in Corelib.ssr.ssrfun]
Tag [section, in Corelib.ssr.ssrfun]
diff --git a/master/corelib/index_global_W.html b/master/corelib/index_global_W.html index f2477cb152..813b41b2b1 100644 --- a/master/corelib/index_global_W.html +++ b/master/corelib/index_global_W.html @@ -772,8 +772,8 @@ Well_founded.R [variable, in Corelib.Init.Wf]
Well_founded.A [variable, in Corelib.Init.Wf]
Well_founded [section, in Corelib.Init.Wf]
-Wf [library]
Wf [library]
+Wf [library]
wlog_neg [lemma, in Corelib.ssr.ssrbool]
wrap [definition, in Corelib.ssr.ssrfun]
wrapped [record, in Corelib.ssr.ssrfun]
diff --git a/master/corelib/index_library_T.html b/master/corelib/index_library_T.html index 94b7fd28a7..f87caa8eea 100644 --- a/master/corelib/index_library_T.html +++ b/master/corelib/index_library_T.html @@ -742,8 +742,8 @@

T (library)

-Tactics
Tactics
+Tactics
Tauto
TransparentState


diff --git a/master/corelib/index_library_W.html b/master/corelib/index_library_W.html index a2903c0bec..fcf7a69e33 100644 --- a/master/corelib/index_library_W.html +++ b/master/corelib/index_library_W.html @@ -742,8 +742,8 @@

W (library)

-Wf
Wf
+Wf