1 files changed, 0 insertions, 326 deletions
diff --git a/contrib/ML4PG/libs/ssreflect/basic/ssrnat_names b/contrib/ML4PG/libs/ssreflect/basic/ssrnat_names
deleted file mode 100644
index 829f9c28..00000000
--- a/contrib/ML4PG/libs/ssreflect/basic/ssrnat_names
+++ /dev/null
@@ -1,326 +0,0 @@
-1 succn_inj
-2 eqnP
-3 eqnE
-4 eqSS
-5 nat_irrelevance
-6 addnE
-7 plusE
-8 add0n
-9 addSn
-10 add1n
-11 addn0
-12 addnS
-13 addSnnS
-14 addnCA
-15 addnC
-16 addn1
-17 addnA
-18 addnAC
-19 addnACA
-20 addn_eq0
-21 eqn_add2l
-22 eqn_add2r
-23 addnI
-24 addIn
-25 addn2
-26 add2n
-27 addn3
-28 add3n
-29 addn4
-30 add4n
-31 subnE
-32 minusE
-33 sub0n
-34 subn0
-35 subnn
-36 subSS
-37 subn1
-38 subn2
-39 subnDl
-40 subnDr
-41 addKn
-42 addnK
-43 subSnn
-44 subnDA
-45 subnAC
-46 subnS
-47 subSKn
-48 ltnS
-49 leq0n
-50 ltn0Sn
-51 ltn0
-52 leqnn
-53 ltnSn
-54 eq_leq
-55 leqnSn
-56 leq_pred
-57 leqSpred
-58 ltn_predK
-59 prednK
-60 leqNgt
-61 ltnNge
-62 ltnn
-63 leqn0
-64 lt0n
-65 lt0n_neq0
-66 eqn0Ngt
-67 neq0_lt0n
-68 eqn_leq
-69 anti_leq
-70 neq_ltn
-71 gtn_eqF
-72 ltn_eqF
-73 leq_eqVlt
-74 ltn_neqAle
-75 leq_trans
-76 leq_ltn_trans
-77 ltnW
-78 leqW
-79 ltn_trans
-80 leq_total
-81 leP
-82 le_irrelevance
-83 ltP
-84 lt_irrelevance
-85 leqP
-86 ltnP
-87 posnP
-88 ltngtP
-89 leq_add2l
-90 ltn_add2l
-91 leq_add2r
-92 ltn_add2r
-93 leq_add
-94 leq_addr
-95 leq_addl
-96 ltn_addr
-97 ltn_addl
-98 addn_gt0
-99 subn_gt0
-100 subn_eq0
-101 leq_subLR
-102 leq_subr
-103 subnKC
-104 subnK
-105 addnBA
-106 subnBA
-107 subKn
-108 subSn
-109 subnSK
-110 leq_sub2r
-111 leq_sub2l
-112 leq_sub
-113 ltn_sub2r
-114 ltn_sub2l
-115 ltn_subRL
-116 subn_if_gt
-117 max0n
-118 maxn0
-119 maxnC
-120 maxnE
-121 maxnAC
-122 maxnA
-123 maxnCA
-124 maxnACA
-125 maxn_idPl
-126 maxn_idPr
-127 maxnn
-128 leq_max
-129 leq_maxl
-130 leq_maxr
-131 gtn_max
-132 geq_max
-133 maxnSS
-134 addn_maxl
-135 addn_maxr
-136 min0n
-137 minn0
-138 minnC
-139 addn_min_max
-140 minnE
-141 minnAC
-142 minnA
-143 minnCA
-144 minnACA
-145 minn_idPl
-146 minn_idPr
-147 minnn
-148 leq_min
-149 gtn_min
-150 geq_min
-151 geq_minl
-152 geq_minr
-153 addn_minr
-154 addn_minl
-155 minnSS
-156 maxnK
-157 maxKn
-158 minnK
-159 minKn
-160 maxn_minl
-161 maxn_minr
-162 minn_maxl
-163 minn_maxr
-164 find_ex_minn
-165 ex_minnP
-166 ex_maxn_subproof
-167 ex_maxnP
-168 eq_ex_minn
-169 eq_ex_maxn
-170 iterSr
-171 iterS
-172 iter_add
-173 iteriS
-174 iteropS
-175 eq_iter
-176 eq_iteri
-177 eq_iterop
-178 multE
-179 mulnE
-180 mul0n
-181 muln0
-182 mul1n
-183 mulSn
-184 mulSnr
-185 mulnS
-186 mulnSr
-187 muln1
-188 mulnC
-189 mulnDl
-190 mulnDr
-191 mulnBl
-192 mulnBr
-193 mulnA
-194 mulnCA
-195 mulnAC
-196 mulnACA
-197 muln_eq0
-198 muln_eq1
-199 muln_gt0
-200 leq_pmull
-201 leq_pmulr
-202 leq_mul2l
-203 leq_mul2r
-204 leq_mul
-205 eqn_mul2l
-206 eqn_mul2r
-207 leq_pmul2l
-208 leq_pmul2r
-209 eqn_pmul2l
-210 eqn_pmul2r
-211 ltn_mul2l
-212 ltn_mul2r
-213 ltn_pmul2l
-214 ltn_pmul2r
-215 ltn_Pmull
-216 ltn_Pmulr
-217 ltn_mul
-218 maxn_mulr
-219 maxn_mull
-220 minn_mulr
-221 minn_mull
-222 expnE
-223 expn0
-224 expn1
-225 expnS
-226 expnSr
-227 exp0n
-228 exp1n
-229 expnD
-230 expnMn
-231 expnM
-232 expnAC
-233 expn_gt0
-234 expn_eq0
-235 ltn_expl
-236 leq_exp2l
-237 ltn_exp2l
-238 eqn_exp2l
-239 expnI
-240 leq_pexp2l
-241 ltn_pexp2l
-242 ltn_exp2r
-243 leq_exp2r
-244 eqn_exp2r
-245 expIn
-246 factE
-247 fact0
-248 factS
-249 fact_gt0
-250 leq_b1
-251 addn_negb
-252 eqb0
-253 lt0b
-254 sub1b
-255 mulnb
-256 oddb
-257 odd_add
-258 odd_sub
-259 odd_opp
-260 odd_mul
-261 odd_exp
-262 doubleE
-263 double0
-264 doubleS
-265 addnn
-266 mul2n
-267 muln2
-268 doubleD
-269 doubleB
-270 leq_double
-271 ltn_double
-272 ltn_Sdouble
-273 leq_Sdouble
-274 odd_double
-275 double_gt0
-276 double_eq0
-277 doubleMl
-278 doubleMr
-279 doubleK
-280 uphalf_double
-281 uphalf_half
-282 odd_double_half
-283 half_bit_double
-284 halfD
-285 half_leq
-286 half_gt0
-287 mulnn
-288 sqrnD
-289 sqrn_sub
-290 sqrnD_sub
-291 subn_sqr
-292 ltn_sqr
-293 leq_sqr
-294 sqrn_gt0
-295 eqn_sqr
-296 sqrn_inj
-297 leqifP
-298 leqif_refl
-299 leqif_trans
-300 monotone_leqif
-301 leqif_geq
-302 leqif_eq
-303 geq_leqif
-304 ltn_leqif
-305 leqif_add
-306 leqif_mul
-307 nat_Cauchy
-308 nat_AGM2
-309 addE
-310 doubleE
-311 add_mulE
-312 mulE
-313 mul_expE
-314 expE
-315 oddE
-316 eq_binP
-317 bin_of_natK
-318 nat_of_binK
-319 nat_of_succ_gt0
-320 nat_of_addn_gt0
-321 nat_of_add_bin
-322 nat_of_mul_bin
-323 nat_of_exp_bin
-324 nat_semi_ring
-325 nat_semi_morph
-326 nat_power_theory