1 files changed, 157 insertions, 0 deletions
diff --git a/coq/ML4PG/libs/ssreflect/advance/bigop_names b/coq/ML4PG/libs/ssreflect/advance/bigop_names
new file mode 100644
index 00000000..d228e3ab
--- /dev/null
+++ b/coq/ML4PG/libs/ssreflect/advance/bigop_names
@@ -0,0 +1,157 @@
+1 mulC_id
+2 mulC_zero
+3 mulC_dist
+4 mul1m
+5 mulm1
+6 mulmA
+7 iteropE
+8 mulmC
+9 mulmCA
+10 mulmAC
+11 mulmACA
+12 mul0m
+13 mulm0
+14 addmA
+15 addmC
+16 addmCA
+17 addmAC
+18 add0m
+19 addm0
+20 mulm_addl
+21 mulm_addr
+22 bigopE
+23 mem_index_iota
+24 mem_index_enum
+25 filter_index_enum
+26 big_load
+27 big_rec3
+28 big_ind3
+29 big_rec2
+30 big_ind2
+31 big_morph
+32 big_rec
+33 big_ind
+34 eq_big_op
+35 big_endo
+36 big_filter
+37 big_filter_cond
+38 eq_bigl
+39 big_andbC
+40 eq_bigr
+41 eq_big
+42 congr_big
+43 big_nil
+44 big_cons
+45 big_map
+46 big_nth
+47 big_hasC
+48 big_pred0_eq
+49 big_pred0
+50 big_cat_nested
+51 big_catl
+52 big_catr
+53 big_const_seq
+54 big_seq_cond
+55 big_seq
+56 eq_big_seq
+57 big_nat_cond
+58 big_nat
+59 congr_big_nat
+60 eq_big_nat
+61 big_geq
+62 big_ltn_cond
+63 big_ltn
+64 big_addn
+65 big_add1
+66 big_nat_recl
+67 big_mkord
+68 big_nat_widen
+69 big_ord_widen_cond
+70 big_ord_widen
+71 big_ord_widen_leq
+72 big_ord0
+73 big_tnth
+74 big_ord_narrow_cond
+75 big_ord_narrow_cond_leq
+76 big_ord_narrow
+77 big_ord_narrow_leq
+78 big_ord_recl
+79 big_const
+80 big_const_nat
+81 big_const_ord
+82 eq_big_idx_seq
+83 eq_big_idx
+84 big1_eq
+85 big1
+86 big1_seq
+87 big_seq1
+88 big_mkcond
+89 big_cat
+90 big_pred1_eq
+91 big_pred1
+92 big_cat_nat
+93 big_nat1
+94 big_nat_recr
+95 big_ord_recr
+96 big_sumType
+97 big_split_ord
+98 eq_big_perm
+99 big_uniq
+100 big_index_uniq
+101 big_rem
+102 big_undup
+103 eq_big_idem
+104 big_split
+105 bigID
+106 bigU
+107 bigD1
+108 bigD1_seq
+109 cardD1x
+110 partition_big
+111 reindex_onto
+112 reindex
+113 reindex_inj
+114 big_nat_rev
+115 pair_big_dep
+116 pair_big
+117 pair_bigA
+118 exchange_big_dep
+119 exchange_big
+120 exchange_big_dep_nat
+121 exchange_big_nat
+122 big_distrl
+123 big_distrr
+124 big_distrlr
+125 big_distr_big_dep
+126 big_distr_big
+127 bigA_distr_big_dep
+128 bigA_distr_big
+129 bigA_distr_bigA
+130 big_has
+131 big_all
+132 big_has_cond
+133 big_all_cond
+134 big_orE
+135 big_andE
+136 sum_nat_const
+137 sum1_card
+138 prod_nat_const
+139 sum_nat_const_nat
+140 prod_nat_const_nat
+141 leqif_sum
+142 leq_sum
+143 sum_nat_eq0
+144 prodn_cond_gt0
+145 prodn_gt0
+146 leq_bigmax_cond
+147 leq_bigmax
+148 bigmax_leqP
+149 bigmax_sup
+150 bigmax_eq_arg
+151 eq_bigmax_cond
+152 eq_bigmax
+153 expn_sum
+154 dvdn_biglcmP
+155 biglcmn_sup
+156 dvdn_biggcdP
+157 biggcdn_inf