1 files changed, 49 insertions, 0 deletions
diff --git a/coq/ML4PG/libs/ssreflect/coqeal/seqmatrix_names b/coq/ML4PG/libs/ssreflect/coqeal/seqmatrix_names
new file mode 100644
index 00000000..694a3a2d
--- /dev/null
+++ b/coq/ML4PG/libs/ssreflect/coqeal/seqmatrix_names
@@ -0,0 +1,49 @@
+1 ord_enum_eqE
+2 eq_mkseqmx_ord
+3 fun_of_seqmxE
+4 mkseqmxE
+5 size_seqmx
+6 seqmxE
+7 seqmx_is_trans
+8 seqmx0n
+9 seqmxm0
+10 inj_seqmx_of_mx
+11 seqmx_eqP
+12 size_row_seqmx
+13 size_row_mkseqmx
+14 seqmxP
+15 seqmx_of_funE
+16 map_seqmxE
+17 zipwithseqmxE
+18 addseqmxE:
+
+19 oppseqmxE:
+
+20 subseqmxE:
+
+21 size_trseqmx
+22 size_row_trseqmx
+23 trseqmxE
+24 const_seqmxE
+25 seqmx0E
+26 minSS
+27 usubseqmxE
+28 dsubseqmxE
+29 lsubseqmxE
+30 rsubseqmxE
+31 ulsubseqmxE
+32 ursubseqmxE
+33 dlsubseqmxE
+34 drsubseqmxE
+35 size_row_row_seqmx
+36 row_seqmxE
+37 size_row_col_seqmx
+38 col_seqmxE
+39 colseqmxE
+40 block_seqmxE
+41 cast_seqmx
+42 scalar_seqmxE
+43 delta_seqmxE
+44 seqmx1E
+45 scaleseqmxE
+46 seqmx_of_mx_eq0