1 files changed, 396 insertions, 0 deletions
diff --git a/coq/ML4PG/libs/ssreflect/advance/matrix_names b/coq/ML4PG/libs/ssreflect/advance/matrix_names
new file mode 100644
index 00000000..41837a27
--- /dev/null
+++ b/coq/ML4PG/libs/ssreflect/advance/matrix_names
@@ -0,0 +1,396 @@
+1 mxE
+2 matrixP
+3 card_matrix
+4 castmx_const
+5 trmx_const
+6 row_perm_const
+7 col_perm_const
+8 xrow_const
+9 xcol_const
+10 rowP
+11 rowK
+12 row_matrixP
+13 colP
+14 row_const
+15 col_const
+16 row'_const
+17 col'_const
+18 col_perm1
+19 row_perm1
+20 col_permM
+21 row_permM
+22 col_row_permC
+23 castmx_id
+24 castmx_comp
+25 castmxK
+26 castmxKV
+27 castmx_sym
+28 castmxE
+29 conform_mx_id
+30 nonconform_mx
+31 conform_castmx
+32 trmxK
+33 trmx_inj
+34 trmx_cast
+35 tr_row_perm
+36 tr_col_perm
+37 tr_xrow
+38 tr_xcol
+39 row_id
+40 col_id
+41 row_eq
+42 col_eq
+43 row'_eq
+44 col'_eq
+45 tr_row
+46 tr_row'
+47 tr_col
+48 tr_col'
+49 row_mxEl
+50 row_mxKl
+51 row_mxEr
+52 row_mxKr
+53 hsubmxK
+54 col_mxEu
+55 col_mxKu
+56 col_mxEd
+57 col_mxKd
+58 eq_row_mx
+59 eq_col_mx
+60 row_mx_const
+61 col_mx_const
+62 trmx_lsub
+63 trmx_rsub
+64 tr_row_mx
+65 tr_col_mx
+66 trmx_usub
+67 trmx_dsub
+68 vsubmxK
+69 cast_row_mx
+70 cast_col_mx
+71 row_mxA
+72 col_mxA
+73 row_row_mx
+74 col_col_mx
+75 row'_row_mx
+76 col'_col_mx
+77 colKl
+78 colKr
+79 rowKu
+80 rowKd
+81 col'Kl
+82 row'Ku
+83 mx'_cast
+84 col'Kr
+85 row'Kd
+86 eq_block_mx
+87 block_mx_const
+88 submxK
+89 block_mxEul
+90 block_mxKul
+91 block_mxEur
+92 block_mxKur
+93 block_mxEdl
+94 block_mxKdl
+95 block_mxEdr
+96 block_mxKdr
+97 block_mxEv
+98 trmx_ulsub
+99 trmx_ursub
+100 trmx_dlsub
+101 trmx_drsub
+102 tr_block_mx
+103 block_mxEh
+104 block_mxA
+105 mxvec_cast
+106 mxvec_indexP
+107 mxvecE
+108 mxvecK
+109 vec_mxK
+110 curry_mxvec_bij
+111 map_trmx
+112 map_const_mx
+113 map_row
+114 map_col
+115 map_row'
+116 map_col'
+117 map_row_perm
+118 map_col_perm
+119 map_xrow
+120 map_xcol
+121 map_castmx
+122 map_conform_mx
+123 map_mxvec
+124 map_vec_mx
+125 map_row_mx
+126 map_col_mx
+127 map_block_mx
+128 map_lsubmx
+129 map_rsubmx
+130 map_usubmx
+131 map_dsubmx
+132 map_ulsubmx
+133 map_ursubmx
+134 map_dlsubmx
+135 map_drsubmx
+136 addmxA
+137 addmxC
+138 add0mx
+139 addNmx
+140 mulmxnE
+141 summxE
+142 const_mx_is_additive
+143 swizzle_mx_is_additive
+144 flatmx0
+145 thinmx0
+146 trmx0
+147 row0
+148 col0
+149 mxvec_eq0
+150 vec_mx_eq0
+151 row_mx0
+152 col_mx0
+153 block_mx0
+154 opp_row_mx
+155 opp_col_mx
+156 opp_block_mx
+157 add_row_mx
+158 add_col_mx
+159 add_block_mx
+160 nz_row_eq0
+161 map_mx0
+162 map_mxN
+163 map_mxD
+164 map_mx_sub
+165 scale1mx
+166 scalemxDl
+167 scalemxDr
+168 scalemxA
+169 scalemx_const
+170 matrix_sum_delta
+171 swizzle_mx_is_scalable
+172 trmx_delta
+173 row_sum_delta
+174 delta_mx_lshift
+175 delta_mx_rshift
+176 delta_mx_ushift
+177 delta_mx_dshift
+178 vec_mx_delta
+179 mxvec_delta
+180 scale_row_mx
+181 scale_col_mx
+182 scale_block_mx
+183 tr_diag_mx
+184 diag_mx_is_linear
+185 diag_mx_sum_delta
+186 diag_const_mx
+187 tr_scalar_mx
+188 trmx1
+189 scalar_mx_is_additive
+190 scale_scalar_mx
+191 scalemx1
+192 scalar_mx_sum_delta
+193 mx1_sum_delta
+194 row1
+195 is_scalar_mxP
+196 scalar_mx_is_scalar
+197 mx0_is_scalar
+198 mx11_scalar
+199 scalar_mx_block
+200 mulmxA
+201 mul0mx
+202 mulmx0
+203 mulmxN
+204 mulNmx
+205 mulmxDl
+206 mulmxDr
+207 mulmxBl
+208 mulmxBr
+209 mulmx_suml
+210 mulmx_sumr
+211 scalemxAl
+212 rowE
+213 row_mul
+214 mulmx_sum_row
+215 mul_delta_mx_cond
+216 mul_delta_mx
+217 mul_delta_mx_0
+218 mul_diag_mx
+219 mul_mx_diag
+220 mulmx_diag
+221 mul_scalar_mx
+222 scalar_mxM
+223 mul1mx
+224 mulmx1
+225 mul_col_perm
+226 mul_row_perm
+227 mul_xcol
+228 col_permE
+229 row_permE
+230 xcolE
+231 xrowE
+232 tr_perm_mx
+233 tr_tperm_mx
+234 perm_mx1
+235 perm_mxM
+236 is_perm_mxP
+237 perm_mx_is_perm
+238 is_perm_mx1
+239 is_perm_mxMl
+240 is_perm_mx_tr
+241 is_perm_mxMr
+242 pid_mx_0
+243 pid_mx_1
+244 pid_mx_row
+245 pid_mx_col
+246 pid_mx_block
+247 tr_pid_mx
+248 pid_mx_minv
+249 pid_mx_minh
+250 mul_pid_mx
+251 pid_mx_id
+252 mul_copid_mx_pid
+253 mul_pid_mx_copid
+254 copid_mx_id
+255 mul_mx_row
+256 mul_col_mx
+257 mul_row_col
+258 mul_col_row
+259 mul_row_block
+260 mul_block_col
+261 mulmx_block
+262 mul_rV_lin1
+263 mul_rV_lin
+264 mul_vec_lin
+265 mx_rV_lin
+266 mx_vec_lin
+267 mulmxr_is_linear
+268 lin_mulmxr_is_linear
+269 mxtrace_tr
+270 mxtrace_is_scalar
+271 mxtrace0
+272 mxtraceD
+273 mxtraceZ
+274 mxtrace_diag
+275 mxtrace_scalar
+276 mxtrace1
+277 trace_mx11
+278 mxtrace_block
+279 matrix_nonzero1
+280 mulmxE
+281 idmxE
+282 scalar_mx_is_multiplicative
+283 lift0_perm0
+284 lift0_perm_lift
+285 lift0_permK
+286 lift0_perm_eq0
+287 lift0_mx_perm
+288 lift0_mx_is_perm
+289 trmx_mul_rev
+290 map_mxZ
+291 map_mxM
+292 map_delta_mx
+293 map_diag_mx
+294 map_scalar_mx
+295 map_mx1
+296 map_perm_mx
+297 map_tperm_mx
+298 map_pid_mx
+299 trace_map_mx
+300 det_map_mx
+301 cofactor_map_mx
+302 map_mx_adj
+303 map_copid_mx
+304 map_mx_is_multiplicative
+305 map_lin1_mx
+306 map_lin_mx
+307 trmx_mul
+308 scalemxAr
+309 mulmx_is_scalable
+310 lin_mulmx_is_linear
+311 lin_mul_row_is_linear
+312 mul_vec_lin_row
+313 mxvec_dotmul
+314 diag_mxC
+315 diag_mx_comm
+316 scalar_mxC
+317 scalar_mx_comm
+318 mul_mx_scalar
+319 mxtrace_mulC
+320 determinant_multilinear
+321 determinant_alternate
+322 det_tr
+323 det_perm
+324 det1
+325 det_mx00
+326 detZ
+327 det0
+328 det_scalar
+329 det_scalar1
+330 det_mulmx
+331 detM
+332 det_diag
+333 expand_cofactor
+334 expand_det_row
+335 cofactor_tr
+336 cofactorZ
+337 expand_det_col
+338 trmx_adj
+339 adjZ
+340 mul_mx_adj
+341 mul_adj_mx
+342 adj1
+343 mulmx1C
+344 mulmx1_min
+345 det_ublock
+346 det_lblock
+347 unitmxE
+348 unitmx1
+349 unitmx_perm
+350 unitmx_tr
+351 unitmxZ
+352 invmx1
+353 invmxZ
+354 invmx_scalar
+355 mulVmx
+356 mulmxV
+357 mulKmx
+358 mulKVmx
+359 mulmxK
+360 mulmxKV
+361 det_inv
+362 unitmx_inv
+363 unitmx_mul
+364 trmx_inv
+365 invmxK
+366 mulmx1_unit
+367 intro_unitmx
+368 invmx_out
+369 detV
+370 unitr_trmx
+371 trmxV
+372 perm_mxV
+373 is_perm_mxV
+374 GL_1E
+375 GL_VE
+376 GL_VxE
+377 GL_ME
+378 GL_MxE
+379 GL_unit
+380 GL_unitmx
+381 GL_det
+382 scalemx_eq0
+383 scalemx_inj
+384 det0P
+385 map_mx_inj
+386 map_mx_is_scalar
+387 map_unitmx
+388 map_mx_unit
+389 map_invmx
+390 map_mx_inv
+391 map_mx_eq0
+392 cormen_lup_perm
+393 cormen_lup_correct
+394 cormen_lup_detL
+395 cormen_lup_lower
+396 cormen_lup_upper