_CoqProject

-Q . LAProof
COQEXTRAFLAGS = "-w -notation-overridden,-ambiguous-paths,-overwriting-delimiting-key,-notation-incompatible-prefix,-deprecated-from-Coq"
  
accuracy_proofs/preamble.v
accuracy_proofs/real_lemmas.v
accuracy_proofs/common.v
accuracy_proofs/float_acc_lems.v
accuracy_proofs/dotprod_model.v
accuracy_proofs/sum_model.v
accuracy_proofs/sum_acc.v
accuracy_proofs/dot_acc_lemmas.v
accuracy_proofs/dot_acc.v
accuracy_proofs/vecnorm_acc.v
accuracy_proofs/fma_dot_acc.v
accuracy_proofs/sum_is_finite.v
accuracy_proofs/fma_is_finite.v
accuracy_proofs/mv_mathcomp.v
accuracy_proofs/gemv_acc.v
accuracy_proofs/vec_op_acc.v
accuracy_proofs/gemm_acc.v
accuracy_proofs/export.v
accuracy_proofs/solve_model.v

C/floatlib.v
C/sparse_model.v
C/sparse.v
C/spec_sparse.v
C/verif_sparse.v
C/verif_sparse_byrows.v
C/VSU_sparse.v
C/cholesky.v
C/verif_cholesky.v
C/alloc.v
C/spec_alloc.v
C/verif_alloc.v
C/densemat.v
C/spec_densemat.v
C/densemat_lemmas.v
C/verif_densemat.v
C/verif_densemat_mult.v
C/verif_densemat_cholesky.v
C/VSU_densemat.v
C/matrix_model.v
C/bandmat.v
C/build_csr.v
C/verif_build_csr.v
C/distinct.v
C/partial_csr.v

C/cblas/ddot.v
C/cblas/ddot_model.v
C/cblas/spec_ddot.v
C/cblas/verif_ddot.v

C/cblas/dasum.v
C/cblas/asum_model.v
C/cblas/spec_dasum.v
C/cblas/verif_dasum.v

C/cblas/dscal.v
C/cblas/scal_model.v
C/cblas/stride_model.v
C/cblas/spec_dscal.v
C/cblas/verif_dscal.v