diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/index_lemma_S.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/index_lemma_S.html')
| -rw-r--r-- | docs/htmldoc/index_lemma_S.html | 94 |
1 files changed, 54 insertions, 40 deletions
diff --git a/docs/htmldoc/index_lemma_S.html b/docs/htmldoc/index_lemma_S.html index 72d70ad..1ef1855 100644 --- a/docs/htmldoc/index_lemma_S.html +++ b/docs/htmldoc/index_lemma_S.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,7 +463,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> <hr/><a name="lemma_S"></a><h2>S (lemma)</h2> @@ -642,13 +642,13 @@ <a href="mathcomp.solvable.burnside_app.html#seqs1">seqs1</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.field.falgebra.html#seqv_sub_adjoin">seqv_sub_adjoin</a> [in <a href="mathcomp.field.falgebra.html">mathcomp.field.falgebra</a>]<br/> <a href="mathcomp.ssreflect.tuple.html#seq_tnthP">seq_tnthP</a> [in <a href="mathcomp.ssreflect.tuple.html">mathcomp.ssreflect.tuple</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#seq_ind2">seq_ind2</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.choice.html#seq_choiceMixin">seq_choiceMixin</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> <a href="mathcomp.ssreflect.choice.html#seq_of_optK">seq_of_optK</a> [in <a href="mathcomp.ssreflect.choice.html">mathcomp.ssreflect.choice</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#seq_sub_axiom">seq_sub_axiom</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.ssreflect.fintype.html#seq_sub_pickleK">seq_sub_pickleK</a> [in <a href="mathcomp.ssreflect.fintype.html">mathcomp.ssreflect.fintype</a>]<br/> <a href="mathcomp.algebra.vector.html#seq1_basis">seq1_basis</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> <a href="mathcomp.algebra.vector.html#seq1_free">seq1_free</a> [in <a href="mathcomp.algebra.vector.html">mathcomp.algebra.vector</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#seq2_ind">seq2_ind</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.solvable.nilpotent.html#series_sol">series_sol</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> <a href="mathcomp.fingroup.action.html#setactE">setactE</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> <a href="mathcomp.fingroup.action.html#setactJ">setactJ</a> [in <a href="mathcomp.fingroup.action.html">mathcomp.fingroup.action</a>]<br/> @@ -835,8 +835,7 @@ <a href="mathcomp.solvable.jordanholder.html#simple_compsP">simple_compsP</a> [in <a href="mathcomp.solvable.jordanholder.html">mathcomp.solvable.jordanholder</a>]<br/> <a href="mathcomp.solvable.gseries.html#simple_maxnormal">simple_maxnormal</a> [in <a href="mathcomp.solvable.gseries.html">mathcomp.solvable.gseries</a>]<br/> <a href="mathcomp.solvable.maximal.html#simple_sol_prime">simple_sol_prime</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> -<a href="mathcomp.field.closed_field.html#sizeTP">sizeTP</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> -<a href="mathcomp.field.closed_field.html#sizeT_qf">sizeT_qf</a> [in <a href="mathcomp.field.closed_field.html">mathcomp.field.closed_field</a>]<br/> +<a href="mathcomp.ssreflect.ssrbool.html#simpl_pred_sortE">simpl_pred_sortE</a> [in <a href="mathcomp.ssreflect.ssrbool.html">mathcomp.ssreflect.ssrbool</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeYE">sizeYE</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeY_mulX">sizeY_mulX</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.algebra.polyXY.html#sizeY_eq0">sizeY_eq0</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> @@ -857,7 +856,10 @@ <a href="mathcomp.algebra.polyXY.html#size_poly_XaY">size_poly_XaY</a> [in <a href="mathcomp.algebra.polyXY.html">mathcomp.algebra.polyXY</a>]<br/> <a href="mathcomp.field.cyclotomic.html#size_Cyclotomic">size_Cyclotomic</a> [in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> <a href="mathcomp.field.cyclotomic.html#size_cyclotomic">size_cyclotomic</a> [in <a href="mathcomp.field.cyclotomic.html">mathcomp.field.cyclotomic</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_permutations">size_permutations</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_tally_seq">size_tally_seq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_allpairs">size_allpairs</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#size_allpairs_dep">size_allpairs_dep</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_reshape">size_reshape</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_flatten">size_flatten</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#size_zip">size_zip</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -898,6 +900,10 @@ <a href="mathcomp.algebra.poly.html#size_comp_poly2">size_comp_poly2</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_comp_poly">size_comp_poly</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_exp">size_exp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_eq1">size_prod_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_seq_eq1">size_prod_seq_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_mul_eq1">size_mul_eq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_prod_seq">size_prod_seq</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_prod">size_prod</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_Cmul">size_Cmul</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_scale">size_scale</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -929,6 +935,7 @@ <a href="mathcomp.algebra.poly.html#size_addl">size_addl</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_add">size_add</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_opp">size_opp</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> +<a href="mathcomp.algebra.poly.html#size_polyC_leq1">size_polyC_leq1</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly1P">size_poly1P</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly_gt0">size_poly_gt0</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> <a href="mathcomp.algebra.poly.html#size_poly_leq0P">size_poly_leq0P</a> [in <a href="mathcomp.algebra.poly.html">mathcomp.algebra.poly</a>]<br/> @@ -975,9 +982,12 @@ <a href="mathcomp.solvable.hall.html#sol_coprime_Sylow_exists">sol_coprime_Sylow_exists</a> [in <a href="mathcomp.solvable.hall.html">mathcomp.solvable.hall</a>]<br/> <a href="mathcomp.solvable.maximal.html#sol_prime_factor_exists">sol_prime_factor_exists</a> [in <a href="mathcomp.solvable.maximal.html">mathcomp.solvable.maximal</a>]<br/> <a href="mathcomp.solvable.nilpotent.html#sol_der1_proper">sol_der1_proper</a> [in <a href="mathcomp.solvable.nilpotent.html">mathcomp.solvable.nilpotent</a>]<br/> +<a href="mathcomp.ssreflect.ssrfun.html#Some_inj">Some_inj</a> [in <a href="mathcomp.ssreflect.ssrfun.html">mathcomp.ssreflect.ssrfun</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_morph">sop_morph</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_spec">sop_spec</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> <a href="mathcomp.solvable.burnside_app.html#sop_inj">sop_inj</a> [in <a href="mathcomp.solvable.burnside_app.html">mathcomp.solvable.burnside_app</a>]<br/> +<a href="mathcomp.ssreflect.path.html#sorted_le_nth">sorted_le_nth</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> +<a href="mathcomp.ssreflect.path.html#sorted_lt_nth">sorted_lt_nth</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#sorted_uniq">sorted_uniq</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#sorted_filter">sorted_filter</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.prime.html#sorted_divisors_ltn">sorted_divisors_ltn</a> [in <a href="mathcomp.ssreflect.prime.html">mathcomp.ssreflect.prime</a>]<br/> @@ -1143,6 +1153,8 @@ <a href="mathcomp.ssreflect.ssrnat.html#subn2">subn2</a> [in <a href="mathcomp.ssreflect.ssrnat.html">mathcomp.ssreflect.ssrnat</a>]<br/> <a href="mathcomp.ssreflect.eqtype.html#SubP">SubP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.algebra.rat.html#subq_ge0">subq_ge0</a> [in <a href="mathcomp.algebra.rat.html">mathcomp.algebra.rat</a>]<br/> +<a href="mathcomp.algebra.interval.html#subr_lersif0r">subr_lersif0r</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> +<a href="mathcomp.algebra.interval.html#subr_lersifr0">subr_lersifr0</a> [in <a href="mathcomp.algebra.interval.html">mathcomp.algebra.interval</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseqP">subseqP</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.path.html#subseq_sorted">subseq_sorted</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> <a href="mathcomp.ssreflect.path.html#subseq_order_path">subseq_order_path</a> [in <a href="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path</a>]<br/> @@ -1151,8 +1163,8 @@ <a href="mathcomp.ssreflect.seq.html#subseq_uniq">subseq_uniq</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_rcons">subseq_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_cons">subseq_cons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> -<a href="mathcomp.ssreflect.seq.html#subseq_refl">subseq_refl</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq_trans">subseq_trans</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#subseq_refl">subseq_refl</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#subseq0">subseq0</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.finset.html#subsetC">subsetC</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#subsetD">subsetD</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> @@ -1352,8 +1364,10 @@ <a href="mathcomp.algebra.mxalgebra.html#summx_sub_sums">summx_sub_sums</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.mxalgebra.html#summx_sub">summx_sub</a> [in <a href="mathcomp.algebra.mxalgebra.html">mathcomp.algebra.mxalgebra</a>]<br/> <a href="mathcomp.algebra.ssrint.html#sumMz">sumMz</a> [in <a href="mathcomp.algebra.ssrint.html">mathcomp.algebra.ssrint</a>]<br/> +<a href="mathcomp.ssreflect.bigop.html#sumnE">sumnE</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_flatten">sumn_flatten</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_rev">sumn_rev</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> +<a href="mathcomp.ssreflect.seq.html#sumn_rot">sumn_rot</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_rcons">sumn_rcons</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_count">sumn_count</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> <a href="mathcomp.ssreflect.seq.html#sumn_cat">sumn_cat</a> [in <a href="mathcomp.ssreflect.seq.html">mathcomp.ssreflect.seq</a>]<br/> @@ -1389,7 +1403,7 @@ <a href="mathcomp.ssreflect.eqtype.html#sum_eqP">sum_eqP</a> [in <a href="mathcomp.ssreflect.eqtype.html">mathcomp.ssreflect.eqtype</a>]<br/> <a href="mathcomp.solvable.cyclic.html#sum_totient_dvd">sum_totient_dvd</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> <a href="mathcomp.solvable.cyclic.html#sum_ncycle_totient">sum_ncycle_totient</a> [in <a href="mathcomp.solvable.cyclic.html">mathcomp.solvable.cyclic</a>]<br/> -<a href="mathcomp.ssreflect.finset.html#sum_nat_dep_const">sum_nat_dep_const</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> +<a href="mathcomp.ssreflect.finset.html#sum_nat_cond_const">sum_nat_cond_const</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.finset.html#sum1dep_card">sum1dep_card</a> [in <a href="mathcomp.ssreflect.finset.html">mathcomp.ssreflect.finset</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#sum1_size">sum1_size</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> <a href="mathcomp.ssreflect.bigop.html#sum1_count">sum1_count</a> [in <a href="mathcomp.ssreflect.bigop.html">mathcomp.ssreflect.bigop</a>]<br/> @@ -1481,7 +1495,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> @@ -1513,14 +1527,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> @@ -1545,7 +1559,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(213 entries)</td> +<td>(221 entries)</td> </tr> <tr> <td>Variable Index</td> @@ -1577,7 +1591,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> @@ -1609,7 +1623,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> @@ -1641,7 +1655,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> @@ -1673,7 +1687,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> @@ -1705,7 +1719,7 @@ <td>Z</td> <td>_</td> <td>other</td> -<td>(47 entries)</td> +<td>(45 entries)</td> </tr> <tr> <td>Inductive Index</td> @@ -1737,14 +1751,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> @@ -1769,7 +1783,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> @@ -1801,7 +1815,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> @@ -1833,7 +1847,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> @@ -1865,14 +1879,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> @@ -1897,7 +1911,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> |