aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/index_notation_F.html
diff options
context:
space:
mode:
authorEnrico Tassi2019-05-22 13:43:08 +0200
committerEnrico Tassi2019-05-22 15:34:14 +0200
commit748d716efb2f2f75946c8386e441ce1789806a39 (patch)
treefe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_notation_F.html
parent415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_notation_F.html')
-rw-r--r--docs/htmldoc/index_notation_F.html232
1 files changed, 116 insertions, 116 deletions
diff --git a/docs/htmldoc/index_notation_F.html b/docs/htmldoc/index_notation_F.html
index cb016d7..9818469 100644
--- a/docs/htmldoc/index_notation_F.html
+++ b/docs/htmldoc/index_notation_F.html
@@ -4,7 +4,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
-<title>mathcomp.ssreflect.tuple</title>
+<title>mathcomp.test_suite.hierarchy_test</title>
</head>
<body>
@@ -47,7 +47,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -79,14 +79,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -111,7 +111,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -143,7 +143,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -175,7 +175,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -207,7 +207,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -239,7 +239,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -271,7 +271,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -303,14 +303,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -335,7 +335,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -367,7 +367,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -399,7 +399,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -431,14 +431,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -463,91 +463,91 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
<hr/><a name="notation_F"></a><h2>F (notation)</h2>
-<a href="mathcomp.field.falgebra.html#22fc78a071967cb498292883560bf256">{ aspace _ } (type_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#7902c4a8ff2316fb35d6d0c2ed7d11ae">'Z ( _ ) (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#cbd9ee36d93894e7e70e23c2d488b443">'C ( _ ) (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#31433815c4b94767dc54e5ea54a78836">'C [ _ ] (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#21d8f2654a27422064fa906a038e93e4">_ ^+ _ (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#e27d7b49f0f266dd87f31a2700ab99c7">_ * _ (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#bcfd974a09004a8a31fe2123e2a5e1bb">[ FalgType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#3c0387428f19a365dfa0c989db9030d7">[ FalgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.character.classfun.html#e936761e50df896498d658058c61dde2">_ ^u</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.field.fieldext.html#5f5a3c95feae5e889ef0ed2ea21bd611">[ fieldExtType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#03c33b945f661e93f536291e742438c3">[ fieldExtType _ of _ ] (form_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d">{ subfield _ } (type_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.field.fieldext.html#43aa599248ac296c93d07d0ece5108b7">_ *F: _</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#e18a3934ddda7b4da23627d05a96af2d">'Cl (action_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#f525fb0dd2275735c0a65da3608bcb12">'e_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#7b6a6a8c01938a6edd22860d7e925339">'R_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#c674f1775e550ca38ba6626787fbdfd2">'n_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#8178faf6fa436d2b11560085cf16b0f2">1 (irrType_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#3cd258bd0038ef00bb5c09c7e22c6159">[ 1 _ ] (irrType_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.field.finfield.html#f360384641878cb2be7294bed4659e99">_ %| _</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
-<a href="mathcomp.field.finfield.html#445fdb3ebc0ff682c0cd1af9d3a32b17">_ ^%:A (ring_scope)</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
-<a href="mathcomp.character.mxabelem.html#4fffb19fcc003d579f537986e6d81a64">'Zm (action_scope)</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09">[ finGroupType of _ ] (form_scope)</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#bdbf19c07c4322c6fcf6df6c95066969">[ baseFinGroupType of _ ] (form_scope)</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#6982596e2b81c072ea7627dbd9786546">_ ^-1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#006ee57122782cbbf25dc03841983bb0">_ * _</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.fingroup.fingroup.html#d998d540958964b9098d14237b8825c5">1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#7c98bb3aae09ec8defcde60e1fe9fd1a">'M (action_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#fc9edd19efe07e751389113a56e73526">'M (groupAction_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946">_ ^@ _ (ring_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#5f85997305decc6e43bdcd4369b88e63">'M (action_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#1665aa361c9febc77836f6e34002c85d">'M (groupAction_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.solvable.finmodule.html#5265ec8bf0e3eb99e5b993065d871eb7">_ ^@ _ (ring_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#820c0d91f14d8bd214791c55fe4916da">, exists _ : _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#16c0991f94f0d812137457fc1c1383fe">, exists _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#a933bbd16e3a45a4b889ac2f8732ec0e">[ exists _ : _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#5404fd9d76c24a375fce91eeeb1972da">[ exists _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#158832d8c1ec7121db752c45c87cc3aa">[ exists ( _ : _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#2622a9930e3eed1321ab6ed4605c7142">[ exists ( _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78">[ exists _ : _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2">[ exists _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#a1fa7fa2f38c8bf7a4380b3099a7f5cc">, forall _ : _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#569613cf8a3bdd9ea86bbbe48a5b61c3">, forall _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#35b77e34a049e8a812164aa2debaf974">[ forall _ : _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#0a2353937835d965c09d6cd592199019">[ forall _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30">[ forall ( _ : _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#71aa9b4d33ee64c2b31b6cd545727657">[ forall ( _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#924e46d1120f21a5b355c376b609abe3">[ forall _ : _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e">[ forall _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#7b05ad85727c891b29b0672026ea07f9">, exists ( _ : _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#5fcc6a9a5ab8cf28a008d132794985d5">, exists ( _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#9a69525d4d7bd01771d4d07ab174d2f1">, exists _ : _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#ef3225e810fcf2e8c51fa9af98d6cdaf">, exists _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#33851fdc2b3107574ff195c5b3a5f91c">, forall ( _ : _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#71e191c4608118a84659c62df77deabc">, forall ( _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#179e9cebf3b372c78d9f6a5df5a9c45d">, forall _ : _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#e66d8de38c2dd41a650467838c8fd364">, forall _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785">, _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#87b50e2524afd24ce3fa86e25e250984">_ ^~</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#ed8677a60b02e6f4a3e034ddedab0754">_ ^*</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#6aaa6b7c692b4350a2b0b8947c625448">[ _ : _ | _ ]</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#8851f797d0e413ad24e2bf680ba67c0f">[ _ | _ ]</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#eb1f7a25d8e03f1f02a5769831d0e74e">[ finType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e">[ finType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#1f3938acab41e5853e751c34c441bf83">[ finAlgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#381777e14bce98b548cb274563c7fc56">[ finComRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#f0aa4fcf143660f4378ecfead8f3fdda">[ finComUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#07fdfbae2c02044f4dae6b5dbeb0c7c7">[ finFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#6c49b73b4d6aa1a932fafe7684bba39c">[ finIdomainType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#f791552e58608a16cb248da4e7f34691">[ finLalgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#73928e07fdf596d7d0d44cccaf9a9cb3">[ finLmodType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#cf58bd711195f609ec57107fc402496c">[ finRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#9af0def31728327fea663946c68b8952">[ finUnitAlgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#7f21453830587186138043335ab91dd1">[ finUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4">[ finGroupType of _ for +%R ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd">[ baseFinGroupType of _ for +%R ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5">[ finZmodType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89">{ ratio _ }</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac">_ %:F</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77">_ %:F</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
-<a href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f">{ fraction _ }</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
+<a href="mathcomp.field.falgebra.html#0ac367aab6864c536e98a34f9ffcfa34">{ aspace _ } (type_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#80354b4ac5a7ae24a2bb90308585eedc">'Z ( _ ) (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#2e0b34a8e05ee287d92de114cd9577b4">'C ( _ ) (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#a3603406613c9df0ee9e7d6a7f7e1386">'C [ _ ] (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#1d427e6c23d5e01e29ecf0123d1e1b59">_ ^+ _ (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#5215eefac650e5069ffc61e3cc9dc055">_ * _ (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#c59cbf7ead4fff233447196845a75eb7">[ FalgType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#8fcc6f073a7a36fa680d6889440e6651">[ FalgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.character.classfun.html#951fc6d5628818da9c9fe35428eee358">_ ^u</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.field.fieldext.html#78069a19fdca27731326a2758b55293c">[ fieldExtType _ of _ for _ ] (form_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
+<a href="mathcomp.field.fieldext.html#702fe37861ef3c9032a715a749ac1ea7">[ fieldExtType _ of _ ] (form_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
+<a href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40">{ subfield _ } (type_scope)</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
+<a href="mathcomp.field.fieldext.html#6f2c77fbfb346ccf3ded84f9624cdaa7">_ *F: _</a> [in <a href="mathcomp.field.fieldext.html">mathcomp.field.fieldext</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#c32b9d64dc405a3e24ead9493c235eac">'Cl (action_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#054dde6e8475b5f978f6fc72d9b3020d">'e_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#fed1998123fd4374722b35d4bd45df37">'R_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#c76c6c26fb72cd04c64ab5deab6af994">'n_ _ (group_ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#8ba1b427d1cc10c412270edbc6cff6dd">1 (irrType_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#40a56b9af2338a1ea7b3f19d7505f6f6">[ 1 _ ] (irrType_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.field.finfield.html#24ae9732afc48da1e1f059fb289af11b">_ %| _</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
+<a href="mathcomp.field.finfield.html#387983a03fdf688b74a29beb3a4344bb">_ ^%:A (ring_scope)</a> [in <a href="mathcomp.field.finfield.html">mathcomp.field.finfield</a>]<br/>
+<a href="mathcomp.character.mxabelem.html#4e8ce2ff912cfeb67343e97564bc5001">'Zm (action_scope)</a> [in <a href="mathcomp.character.mxabelem.html">mathcomp.character.mxabelem</a>]<br/>
+<a href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a">[ finGroupType of _ ] (form_scope)</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
+<a href="mathcomp.fingroup.fingroup.html#ac5c214a3d709d8519333b0f98027cc9">[ baseFinGroupType of _ ] (form_scope)</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
+<a href="mathcomp.fingroup.fingroup.html#956536dc58c202e68942118494784d7d">_ ^-1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
+<a href="mathcomp.fingroup.fingroup.html#102ef8aeb14816079aff70619dedce2e">_ * _</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
+<a href="mathcomp.fingroup.fingroup.html#1944280a1d5c9fe870f1187d525b73f2">1</a> [in <a href="mathcomp.fingroup.fingroup.html">mathcomp.fingroup.fingroup</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#75180d85ac3b996e23d5f700ff669508">'M (action_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#60648ddfb848055c00656b4851a7ea06">'M (groupAction_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#a8d159da9722ccf39a3be9874c41f224">_ ^@ _ (ring_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#e64e8beaaa33e98dbf15c1c648c8e8fa">'M (action_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#523346788a5254daf6c0408c3a5dc259">'M (groupAction_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.solvable.finmodule.html#2b9e94cf53d24eee473cd33f39783e94">_ ^@ _ (ring_scope)</a> [in <a href="mathcomp.solvable.finmodule.html">mathcomp.solvable.finmodule</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#0145806588c5e908657ca7bbbf7abd16">, exists _ : _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#919732e2a395b004050c56ad6129fab5">, exists _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#251e8192c305cd7601bbed67fd6d6249">[ exists _ : _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#f302e204901821a508e6d6d00228c0ed">[ exists _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#14d06eec1f5f7dfac346d730fae6723c">[ exists ( _ : _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#e9122b3568d6f47f958b76a6e55e4e40">[ exists ( _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482">[ exists _ : _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25">[ exists _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#c6e0bc4114dd714e7262ed511d975a84">, forall _ : _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#7406769ad390d6c18d532b497e931ef0">, forall _ in _ _ (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#e786d38fb1c78583c78486483761dfff">[ forall _ : _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f">[ forall _ in _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#b14c43cd248537980c3a1a815ab087df">[ forall ( _ : _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#90a753c4c9a43b6ba4178e7bc1e47801">[ forall ( _ | _ ) _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#fb0199913c9911d56fa87965a9a828a3">[ forall _ : _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6">[ forall _ _ ] (bool_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#3b2dca918c748246f164f2487e80f224">, exists ( _ : _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#e38196bd288251be5369c1e4ce7316f7">, exists ( _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#5675e9c5cf174e09b1b7005056e9bd89">, exists _ : _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#879ea41111b984d072ab3bba11feda79">, exists _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#e43a13e3d639c464aa3578ee61719a3b">, forall ( _ : _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#59ce155014a925cca079058b40bab72e">, forall ( _ | _ ) _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#e1924a831ebc4eede7a49ea158a3d66c">, forall _ : _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#491573e303f379eb171e60e73aff62ae">, forall _ _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98">, _ (fin_quant_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#56df6c3db37fd477fd0b9e866d6c43d1">_ ^~</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#ea5146b504820609501c18972cdc0754">_ ^*</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#a144991985dddee1fffe479e66e76aa4">[ _ : _ | _ ]</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#fee710af89d70df72664de2598d9dce0">[ _ | _ ]</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f">[ finType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.ssreflect.fintype.html#274683adfd1c9a24b44d4dd6ea30913a">[ finType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#e1046e375fa30252214f407945285be1">[ finAlgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#b13c97e55bebdc1c181a99b80106c099">[ finComRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#29c2dac4b2cace3201f3f23b551d143a">[ finComUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#85a9f33cca8b2a31e30517c43d5ecb47">[ finFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#762465ada9848b70124d860dd97a755c">[ finIdomainType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#006f6a476eaf49ff2271764c2e9c0634">[ finLalgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#89ed2b9c4fe0e2b73b78eb3dc17a4b6f">[ finLmodType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#dfd62d789441026daed4d1ea30e2ff11">[ finRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#2aaa42abe766947d0080d3fd1521c4bc">[ finUnitAlgType _ of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#157b0761db3726d8e1bc0a71108dc48f">[ finUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#a37f16a335f7a3ac65f83e3545c3e50c">[ finGroupType of _ for +%R ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#d6b25f501b9fb5e9b743073d52f24511">[ baseFinGroupType of _ for +%R ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.finalg.html#144f70011c058d1c741eaa431b4b8944">[ finZmodType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.finalg.html">mathcomp.algebra.finalg</a>]<br/>
+<a href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc">{ ratio _ }</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
+<a href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d">_ %:F</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
+<a href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6">_ %:F</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
+<a href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce">{ fraction _ }</a> [in <a href="mathcomp.algebra.fraction.html">mathcomp.algebra.fraction</a>]<br/>
<br/><br/><hr/><table>
<tr>
<td>Global Index</td>
@@ -579,7 +579,7 @@
<td><a href="index_global_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_global_*.html">other</a></td>
-<td>(23233 entries)</td>
+<td>(23836 entries)</td>
</tr>
<tr>
<td>Notation Index</td>
@@ -611,14 +611,14 @@
<td><a href="index_notation_Z.html">Z</a></td>
<td>_</td>
<td><a href="index_notation_*.html">other</a></td>
-<td>(1373 entries)</td>
+<td>(1409 entries)</td>
</tr>
<tr>
<td>Module Index</td>
<td><a href="index_module_A.html">A</a></td>
<td><a href="index_module_B.html">B</a></td>
<td><a href="index_module_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_module_D.html">D</a></td>
<td><a href="index_module_E.html">E</a></td>
<td><a href="index_module_F.html">F</a></td>
<td><a href="index_module_G.html">G</a></td>
@@ -643,7 +643,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(213 entries)</td>
+<td>(221 entries)</td>
</tr>
<tr>
<td>Variable Index</td>
@@ -675,7 +675,7 @@
<td><a href="index_variable_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3475 entries)</td>
+<td>(3574 entries)</td>
</tr>
<tr>
<td>Library Index</td>
@@ -707,7 +707,7 @@
<td><a href="index_library_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(89 entries)</td>
+<td>(90 entries)</td>
</tr>
<tr>
<td>Lemma Index</td>
@@ -739,7 +739,7 @@
<td><a href="index_lemma_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(11853 entries)</td>
+<td>(12096 entries)</td>
</tr>
<tr>
<td>Constructor Index</td>
@@ -771,7 +771,7 @@
<td><a href="index_constructor_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(359 entries)</td>
+<td>(368 entries)</td>
</tr>
<tr>
<td>Axiom Index</td>
@@ -803,7 +803,7 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(47 entries)</td>
+<td>(45 entries)</td>
</tr>
<tr>
<td>Inductive Index</td>
@@ -835,14 +835,14 @@
<td>Z</td>
<td>_</td>
<td>other</td>
-<td>(103 entries)</td>
+<td>(107 entries)</td>
</tr>
<tr>
<td>Projection Index</td>
<td><a href="index_projection_A.html">A</a></td>
<td><a href="index_projection_B.html">B</a></td>
<td><a href="index_projection_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_projection_D.html">D</a></td>
<td><a href="index_projection_E.html">E</a></td>
<td><a href="index_projection_F.html">F</a></td>
<td><a href="index_projection_G.html">G</a></td>
@@ -867,7 +867,7 @@
<td><a href="index_projection_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(266 entries)</td>
+<td>(273 entries)</td>
</tr>
<tr>
<td>Section Index</td>
@@ -899,7 +899,7 @@
<td><a href="index_section_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(1118 entries)</td>
+<td>(1140 entries)</td>
</tr>
<tr>
<td>Abbreviation Index</td>
@@ -931,7 +931,7 @@
<td><a href="index_abbreviation_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(691 entries)</td>
+<td>(728 entries)</td>
</tr>
<tr>
<td>Definition Index</td>
@@ -963,14 +963,14 @@
<td><a href="index_definition_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(3461 entries)</td>
+<td>(3596 entries)</td>
</tr>
<tr>
<td>Record Index</td>
<td><a href="index_record_A.html">A</a></td>
<td>B</td>
<td><a href="index_record_C.html">C</a></td>
-<td>D</td>
+<td><a href="index_record_D.html">D</a></td>
<td><a href="index_record_E.html">E</a></td>
<td><a href="index_record_F.html">F</a></td>
<td><a href="index_record_G.html">G</a></td>
@@ -995,7 +995,7 @@
<td><a href="index_record_Z.html">Z</a></td>
<td>_</td>
<td>other</td>
-<td>(185 entries)</td>
+<td>(189 entries)</td>
</tr>
</table>
</div>