Moving ML4PG from coq directory to contrib directory.

1 files changed, 394 insertions, 0 deletions

diff --git a/contrib/ML4PG/libs/ssreflect/basic/seq_names b/contrib/ML4PG/libs/ssreflect/basic/seq_names
new file mode 100644
index 00000000..9ad9bc21
--- /dev/null
+++ b/contrib/ML4PG/libs/ssreflect/basic/seq_names
@@ -0,0 +1,394 @@
+1 size0nil
+2 nilP
+3 size_behead
+4 size_ncons
+5 size_nseq
+6 cat0s
+7 cat1s
+8 cat_cons
+9 cat_nseq
+10 cats0
+11 catA
+12 size_cat
+13 rcons_cons
+14 cats1
+15 lastI
+16 last_cons
+17 size_rcons
+18 size_belast
+19 last_cat
+20 last_rcons
+21 belast_cat
+22 belast_rcons
+23 cat_rcons
+24 rcons_cat
+25 lastP
+26 last_ind
+27 nth0
+28 nth_default
+29 nth_nil
+30 last_nth
+31 nth_last
+32 nth_behead
+33 nth_cat
+34 nth_rcons
+35 nth_ncons
+36 nth_nseq
+37 eq_from_nth
+38 size_set_nth
+39 set_nth_nil
+40 nth_set_nth
+41 set_set_nth
+42 count_filter
+43 has_count
+44 count_size
+45 all_count
+46 filter_all
+47 all_filterP
+48 filter_id
+49 has_find
+50 find_size
+51 find_cat
+52 has_nil
+53 has_seq1
+54 has_seqb
+55 all_nil
+56 all_seq1
+57 nth_find
+58 before_find
+59 filter_cat
+60 filter_rcons
+61 count_cat
+62 has_cat
+63 has_rcons
+64 all_cat
+65 all_rcons
+66 eq_find
+67 eq_filter
+68 eq_count
+69 eq_has
+70 eq_all
+71 sub_find
+72 sub_has
+73 sub_count
+74 sub_all
+75 filter_pred0
+76 filter_predT
+77 filter_predI
+78 count_pred0
+79 count_predT
+80 count_predUI
+81 count_predC
+82 has_pred0
+83 has_predT
+84 has_predC
+85 has_predU
+86 all_pred0
+87 all_predT
+88 all_predC
+89 all_predI
+90 drop_behead
+91 drop0
+92 drop1
+93 drop_oversize
+94 drop_size
+95 drop_cons
+96 size_drop
+97 drop_cat
+98 drop_size_cat
+99 nconsK
+100 take0
+101 take_oversize
+102 take_size
+103 take_cons
+104 drop_rcons
+105 cat_take_drop
+106 size_takel
+107 size_take
+108 take_cat
+109 take_size_cat
+110 takel_cat
+111 nth_drop
+112 nth_take
+113 drop_nth
+114 take_nth
+115 rot0
+116 size_rot
+117 rot_oversize
+118 rot_size
+119 has_rot
+120 rot_size_cat
+121 rotK
+122 rot_inj
+123 rot1_cons
+124 catrev_catl
+125 catrev_catr
+126 catrevE
+127 rev_cons
+128 size_rev
+129 rev_cat
+130 rev_rcons
+131 revK
+132 nth_rev
+133 eqseqP
+134 eqseqE
+135 eqseq_cons
+136 eqseq_cat
+137 eqseq_rcons
+138 has_filter
+139 size_eq0
+140 in_cons
+141 in_nil
+142 mem_seq1
+143 mem_seq2
+144 mem_seq3
+145 mem_seq4
+146 mem_cat
+147 mem_rcons
+148 mem_head
+149 mem_last
+150 mem_behead
+151 mem_belast
+152 mem_nth
+153 mem_take
+154 mem_drop
+155 mem_rev
+156 hasP
+157 hasPn
+158 allP
+159 allPn
+160 mem_filter
+161 eq_in_filter
+162 eq_in_find
+163 eq_in_count
+164 eq_in_all
+165 eq_in_has
+166 eq_has_r
+167 eq_all_r
+168 has_sym
+169 has_pred1
+170 all_pred1P
+171 all_pred1_constant
+172 all_pred1_nseq
+173 constant_nseq
+174 constantP
+175 cons_uniq
+176 cat_uniq
+177 uniq_catC
+178 uniq_catCA
+179 rcons_uniq
+180 filter_uniq
+181 rot_uniq
+182 rev_uniq
+183 count_uniq_mem
+184 filter_pred1_uniq
+185 size_undup
+186 mem_undup
+187 undup_uniq
+188 undup_id
+189 ltn_size_undup
+190 filter_undup
+191 index_size
+192 index_mem
+193 nth_index
+194 index_cat
+195 index_uniq
+196 index_head
+197 index_last
+198 nth_uniq
+199 mem_rot
+200 eqseq_rot
+201 rot_to
+202 nthP
+203 has_nthP
+204 all_nthP
+205 set_nth_default
+206 headI
+207 nth_incr_nth
+208 size_incr_nth
+209 perm_eqP
+210 perm_eq_refl
+211 perm_eq_sym
+212 perm_eq_trans
+213 perm_eqlE
+214 perm_eqlP
+215 perm_eqrP
+216 perm_catC
+217 perm_cat2l
+218 perm_cons
+219 perm_cat2r
+220 perm_catAC
+221 perm_catCA
+222 perm_rcons
+223 perm_rot
+224 perm_rotr
+225 perm_filterC
+226 perm_eq_mem
+227 perm_eq_size
+228 perm_eq_small
+229 uniq_leq_size
+230 leq_size_uniq
+231 uniq_size_uniq
+232 leq_size_perm
+233 perm_uniq
+234 perm_eq_uniq
+235 uniq_perm_eq
+236 count_mem_uniq
+237 catCA_perm_ind
+238 catCA_perm_subst
+239 size_rotr
+240 mem_rotr
+241 rotr_size_cat
+242 rotr1_rcons
+243 has_rotr
+244 rotr_uniq
+245 rotrK
+246 rotr_inj
+247 rev_rot
+248 rev_rotr
+249 rot_addn
+250 rotS
+251 rot_add_mod
+252 rot_rot
+253 rot_rotr
+254 rotr_rotr
+255 mask_false
+256 mask_true
+257 mask0
+258 mask1
+259 mask_cons
+260 size_mask
+261 mask_cat
+262 has_mask_cons
+263 has_mask
+264 mask_rot
+265 mem_mask_cons
+266 mem_mask
+267 mask_uniq
+268 mem_mask_rot
+269 sub0seq
+270 subseq0
+271 subseqP
+272 subseq_trans
+273 subseq_refl
+274 cat_subseq
+275 prefix_subseq
+276 suffix_subseq
+277 mem_subseq
+278 sub1seq
+279 size_subseq
+280 size_subseq_leqif
+281 subseq_cons
+282 subseq_rcons
+283 subseq_uniq
+284 rem_id
+285 perm_to_rem
+286 size_rem
+287 rem_subseq
+288 rem_uniq
+289 mem_rem
+290 rem_filter
+291 mem_rem_uniq
+292 map_cons
+293 map_nseq
+294 map_cat
+295 size_map
+296 behead_map
+297 nth_map
+298 map_rcons
+299 last_map
+300 belast_map
+301 filter_map
+302 find_map
+303 has_map
+304 all_map
+305 count_map
+306 map_take
+307 map_drop
+308 map_rot
+309 map_rotr
+310 map_rev
+311 map_mask
+312 inj_map
+313 filter_mask
+314 filter_subseq
+315 subseq_filter
+316 subseq_uniqP
+317 perm_to_subseq
+318 map_f
+319 mapP
+320 map_uniq
+321 map_inj_in_uniq
+322 map_subseq
+323 nth_index_map
+324 perm_map
+325 mem_map
+326 index_map
+327 map_inj_uniq
+328 map_of_seq
+329 map_id
+330 eq_map
+331 map_comp
+332 mapK
+333 eq_in_map
+334 map_id_in
+335 map_pK
+336 size_pmap
+337 pmapS_filter
+338 pmap_filter
+339 eq_pmap
+340 mem_pmap
+341 can2_mem_pmap
+342 pmap_uniq
+343 size_pmap_sub
+344 mem_pmap_sub
+345 pmap_sub_uniq
+346 size_iota
+347 iota_add
+348 iota_addl
+349 nth_iota
+350 mem_iota
+351 iota_uniq
+352 size_mkseq
+353 eq_mkseq
+354 nth_mkseq
+355 mkseq_nth
+356 mkseq_uniq
+357 perm_eq_iotaP
+358 foldr_cat
+359 foldr_map
+360 sumn_nseq
+361 sumn_cat
+362 natnseq0P
+363 foldl_rev
+364 foldl_cat
+365 size_pairmap
+366 pairmap_cat
+367 nth_pairmap
+368 size_scanl
+369 scanl_cat
+370 nth_scanl
+371 scanlK
+372 pairmapK
+373 zip_unzip
+374 unzip1_zip
+375 unzip2_zip
+376 size1_zip
+377 size2_zip
+378 size_zip
+379 zip_cat
+380 nth_zip
+381 nth_zip_cond
+382 zip_rcons
+383 rev_zip
+384 size_flatten
+385 flatten_cat
+386 flattenK
+387 reshapeKr
+388 reshapeKl
+389 size_allpairs
+390 allpairs_cat
+391 allpairsP
+392 mem_allpairs
+393 allpairs_catr
+394 allpairs_uniq