_CoqProject

-R . Iterative
lemmas.v
inf_norm_properties.v
floatlib.v
jacob_list_fun_model.v
fma_dot_mat_model.v
fma_floating_point_model.v
fma_real_func_model.v


StationaryMethods/common.v
StationaryMethods/op_defs.v
StationaryMethods/float_acc_lems.v
StationaryMethods/list_lemmas.v
StationaryMethods/dotprod_model.v
StationaryMethods/sum_model.v
StationaryMethods/fma_dot_acc.v
StationaryMethods/fma_is_finite.v

finite_lemmas_additional.v
norm_compat.v
fma_matrix_vec_mult.v
vec_sum_inf_norm_rel.v
fma_jacobi_forward_error.v
bound_on_x.v
jacobi_preconditions.v
diag_invertibility.v
jacobi_iteration_bound.v


sparse/sparse.v
sparse/spec_sparse.v
sparse/verif_sparse.v
sparse/verif_sparse_byrows.v
sparse/jacobi.v
sparse/spec_jacobi.v
sparse/verif_jacobi.v
sparse/verif_jacobi2.v
sparse/sparse_model.v
sparse/fun_model_lemmas.v
sparse/vst_improvements.v
sparse/main.v
sparse/distinct.v
sparse/build_csr.v
sparse/build_csr2.v
sparse/spec_build_csr.v
sparse/partial_csr.v
sparse/verif_build_csr.v
sparse/verif_build_csr2.v
sparse/verif_quicksort.v