1 files changed, 45 insertions, 42 deletions
diff --git a/docs/htmldoc/index_notation_C.html b/docs/htmldoc/index_notation_C.html
index c6588f3..d494774 100644
--- a/docs/htmldoc/index_notation_C.html
+++ b/docs/htmldoc/index_notation_C.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,34 +463,37 @@
 <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_C"></a><h2>C (notation)</h2>
-<a href="mathcomp.character.mxrepresentation.html#333123aecb84dc536c58a58868f7e94f">_ ^f (ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.character.mxrepresentation.html#b0f826e6b28b62b07de0a7ecb715959e">_ ^f (ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
-<a href="mathcomp.fingroup.automorphism.html#fc41e85c800db79ed681728de9fb8a9b">_ \char _</a> [in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/>
-<a href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3">[ choiceType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
-<a href="mathcomp.ssreflect.choice.html#3c4bcf103732e5c03bac4c26d0c2ac12">[ choiceType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
-<a href="mathcomp.character.classfun.html#6eaebbc3606793e006c3e4f06a0b870e">'1_ _</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.field.falgebra.html#98e8399dc171f0712bc513d630fa7681"><< _ ; _ >> (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.field.falgebra.html#177559ff502b98bbdadd6a453347ab47"><< _ & _ >> (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
-<a href="mathcomp.ssreflect.choice.html#c3b3d63d167c5615b729c64355a588ab">[ rec _ , _ , _ ]</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
-<a href="mathcomp.character.inertia.html#5e2f669c7c6efc62ca0beee8eac18421">` T (group_scope)</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
-<a href="mathcomp.fingroup.quotient.html#90c786ff7a60565c6e58078021fae18c">_ / _ (Group_scope)</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
-<a href="mathcomp.character.classfun.html#099f1d51f6746a815b66f1e730406302">_ %% B (cfun_scope)</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.character.classfun.html#3d16f1424bbc75f166996053a9778514">_ / B (cfun_scope)</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
-<a href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c">[ countType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
-<a href="mathcomp.ssreflect.choice.html#45eb30de99675fc3a25ff0fa8a76c46a">[ countType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
-<a href="mathcomp.field.countalg.html#6e1bcdb9d1dbca5fb56c1ef5bd06c0a1">[ countClosedFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#1dfc3bd15cbad77b60ee2156a3520c8b">[ countComRingType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#f31de580ef70de9f9efa0f0455fc600b">[ countComUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#7620d5c11cdd558b0330c47dad0b0681">[ countDecFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#55a09bbf18b19424c74b103d26a5c4b0">[ countFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#e009becc591cb361eca4588336d0f9d8">[ countIdomainType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#b8f3d358caffeab4b18f72af97657654">[ countRingType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#182b62279b716241802fba985969ecd2">[ countUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
-<a href="mathcomp.field.countalg.html#04d2f82770d2c7b3524ac143877824a7">[ countZmodType of _ ] (form_scope)</a> [in <a href="mathcomp.field.countalg.html">mathcomp.field.countalg</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#ba0a667eed4af88c4a40c36abce10db5">_ ^f (ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.character.mxrepresentation.html#62fc53b312b1b9229e2dbc4a50119819">_ ^f (ring_scope)</a> [in <a href="mathcomp.character.mxrepresentation.html">mathcomp.character.mxrepresentation</a>]<br/>
+<a href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba">_ \char _</a> [in <a href="mathcomp.fingroup.automorphism.html">mathcomp.fingroup.automorphism</a>]<br/>
+<a href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328">[ choiceType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
+<a href="mathcomp.ssreflect.choice.html#5aecd629a84e4074bfe0a7de23c55d82">[ choiceType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
+<a href="mathcomp.character.classfun.html#a2e268216161616d418b1dd69313ec2b">'1_ _</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.field.closed_field.html#009e3de166439b72aa502f1767bda5b6">_ ->_ _ _</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
+<a href="mathcomp.field.closed_field.html#b8e0aff366eebb2a3e936a17d5d6b4cf">'if _ then _ else _</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
+<a href="mathcomp.field.closed_field.html#9aa131ff55a792756fd3ade7420bfe48">'let _ <- _ ; _</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/>
+<a href="mathcomp.field.falgebra.html#71a48dd0de7f83d8b3db34800dc1ee2d"><< _ ; _ >> (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.field.falgebra.html#77ea2a1af80620c45e915838c6b4069e"><< _ & _ >> (vspace_scope)</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/>
+<a href="mathcomp.ssreflect.choice.html#9f7afcf8f8bed7601295f21ad4549fa6">[ rec _ , _ , _ ]</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
+<a href="mathcomp.character.inertia.html#5219cefec0fc801efe928dc901f7eee3">` T (group_scope)</a> [in <a href="mathcomp.character.inertia.html">mathcomp.character.inertia</a>]<br/>
+<a href="mathcomp.fingroup.quotient.html#493413ea064c0febba0be7abef6c554d">_ / _ (Group_scope)</a> [in <a href="mathcomp.fingroup.quotient.html">mathcomp.fingroup.quotient</a>]<br/>
+<a href="mathcomp.character.classfun.html#57f3294a3433a9d6d9da43648e3842d3">_ %% B (cfun_scope)</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.character.classfun.html#f776f4454e0f767d03ceed800abc137e">_ / B (cfun_scope)</a> [in <a href="mathcomp.character.classfun.html">mathcomp.character.classfun</a>]<br/>
+<a href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8">[ countType of _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
+<a href="mathcomp.ssreflect.choice.html#6b64a8182e19cfcfdb25b3be2b7f0d83">[ countType of _ for _ ] (form_scope)</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#92d3da17aa257b243e0b4add5f350442">[ countClosedFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#d271043791f97708a05788e885686caa">[ countComRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#6e623071866dc1a29a10d36cc1dfa886">[ countComUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#1ab55886e2b992f0c2d8591f02a7baf7">[ countDecFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#7ca0985aed2b28afaaa4007eb0a80f3a">[ countFieldType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#deee2c5961371227bcb71bc712dbd08f">[ countIdomainType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#5d38f59e59d31b0f5328b7330ff4d0f6">[ countRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#d7279d52944865f8d2b1e61af96c64e0">[ countUnitRingType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
+<a href="mathcomp.algebra.countalg.html#c4cf911b6276243d26c2dd85fdb53f8f">[ countZmodType of _ ] (form_scope)</a> [in <a href="mathcomp.algebra.countalg.html">mathcomp.algebra.countalg</a>]<br/>
 <br/><br/></div>
 
 <div id="footer">