VeriNum · ak-2485 · Mar 12, 2026 · Mar 7, 2026 · Mar 10, 2026
diff --git a/.gitignore b/.gitignore
@@ -8,6 +8,7 @@ Makefile.coq
 Makefile.coq.conf
 CoqMakefile
 CoqMakefile.conf
+.history/*
 .*.aux
 .*.d
 *.a
@@ -48,3 +49,4 @@ html/LAProof.*
 html/genindex.html
 html/*.css
 html/toc.html
+.vscode/settings.json
diff --git a/C/matrix_model.v b/C/matrix_model.v
@@ -32,9 +32,6 @@ Unset Printing Implicit Defensive.
 Set Bullet Behavior "Strict Subproofs".
 (* end show *)
 
-Definition neg_zero {t}: ftype t := Binary.B754_zero (fprec t) (femax t) true.
-
-
 Lemma map_inj: forall [T1 T2] (f: T1 -> T2) (H: injective f) (al bl: list T1), map f al = map f bl -> al=bl.
 Proof.
 induction al; destruct bl; simpl; intros; inversion H0; clear H0; subst; auto.

diff --git a/C/spec_densemat.v b/C/spec_densemat.v
@@ -353,7 +353,7 @@ Definition densemat_clear_spec :=
    program correct, there's no need for dynamic bounds checking.  
 
   The precondition of the function enforces that [0 <= i < m] and [0 <= j < n].  It does so by construction
-   of the dependently typed value [X], where the last component is a pair [(i: 'I_[m], j: 'I[n]).
+   of the dependently typed value [X], where the last component is a pair [(i: 'I_[m], j: 'I[n])].
     *)
 Definition densematn_get_spec :=
   DECLARE _densematn_get

diff --git a/C/verif_densemat_cholesky.v b/C/verif_densemat_cholesky.v
@@ -323,7 +323,7 @@ forward_for_simple_bound (Z.of_nat n) (EX i:Z,
   set (al := seq.foldl _ _ _).
   subst bi. change (fstep i)  with al.
   unfold forward_subst_step.
-  change ssralg.GRing.zero with (@ord0 O).
+ (* change ssralg.GRing.zero with (@ord0 O). *)  (* MathComp 2.4 *)
   change @seq.map with @map.
   rewrite take_sublist.
   set (uu := BDIV _ _).

diff --git a/C/verif_sparse_byrows.v b/C/verif_sparse_byrows.v
@@ -175,7 +175,7 @@ forward_for_simple_bound (Zlength mval)
    unfold matrix_rows; subst i. clear H10 H11 H12 H13 H9 H8 PNp PNv PNm H6.
     list_solve.
 -
- Intro result. Exists result.
+ Intro r; Exists r.
  unfold matrix_rows in *. list_simplify.
  entailer!.
  unfold matrix_vector_mult in H9 |- *.

diff --git a/How-to-document.md b/How-to-document.md
@@ -2,11 +2,13 @@
 
 ## Rocq documentation (in .v files)
 
-1.  Edit html/index.html as you see fit.  Do not edit any files of the form html/LAProof.*, as these are automatically generated by coqdoc.
+0. Because Makefile.coq's "make clean" removes the entire html directory, we cannot store the reference copy of index.html there.  Instead, index.html is in the root directory, and copied into the html directory by "make html2".
+
+1.  Edit index.html as you see fit.  Do not edit any files of the form html/LAProof.*, as these are automatically generated by coqdoc.
 
 2.  Edit the comments in any of the .v files, using [Coqdoc markup](https://rocq-prover.org/doc/V8.20.0/refman/using/tools/coqdoc.html).
 
-3.  `make html` creates all the Coqdoc output in the html/ directory.  Browse and review these local files (by doing `open file` in your browser) and edit the .v files until this looks the way you want it.
+3.  `make html2` creates all the Coqdoc output in the html/ directory.  Browse and review these local files (by doing `open file` in your browser) and edit the .v files until this looks the way you want it.
 
 4.  `make publish` sends all those html files (including index.html if you have edited it) to the Github pages site at https://verinum.org/LAProof/.  The way it does this is by committing them to the special gh-pages branch of this repo, which contains _only_ a docs directory with those HTML files.  After you do `make publish`, it will take several minutes before the changes appear at verinum.org/LAProof.
 

diff --git a/Makefile.coq.local b/Makefile.coq.local
@@ -1,10 +1,15 @@
 # COQDOC publishing
-COQDOCEXTRAFLAGS= -g --no-lib-name --index genindex --lib-subtitles --interpolate -utf8
+COQDOCEXTRAFLAGS= -g --no-lib-name --with-header header.html --index genindex --lib-subtitles --interpolate -utf8
 
 accuracy: accuracy_proofs/export.vo
 C: C/verif_alloc.vo C/verif_sparse.vo C/verif_sparse_byrows.vo C/VSU_densemat.vo C/verif_build_csr.vo
 
-publish: html cdocs
+#  Ugh.  We can't just store the reference copy of index.html in html/index.html, because Makefile.coq's
+#   standard "make clean" removes the html directory entirely.  So we gotta do this hack:
+html2: html index.html
+	cp index.html html/index.html
+
+publish: html2 cdocs
 	cd gh-pages; git submodule update
 	cd gh-pages; rm -rf docs; mkdir docs
 	cp html/* gh-pages/docs

diff --git a/_CoqProject b/_CoqProject
@@ -2,6 +2,7 @@
 COQEXTRAFLAGS = "-w -notation-overridden,-ambiguous-paths,-overwriting-delimiting-key,-notation-incompatible-prefix"
 
 accuracy_proofs/preamble.v
+accuracy_proofs/real_lemmas.v
 accuracy_proofs/common.v
 accuracy_proofs/float_acc_lems.v
 accuracy_proofs/dotprod_model.v
@@ -11,6 +12,7 @@ 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