diff --git a/OLD_LICENSE b/OLD_LICENSE
index a7e94d6..da98894 100644
--- a/OLD_LICENSE
+++ b/OLD_LICENSE
@@ -2,7 +2,7 @@ How VCFloat became LGPL licensed instead of GPL licensed: a History
 
 VCFloat, a Coq Framework for verifying floating-point computations,
 was originally developed by researchers at Reservoir Labs Inc.
-It was copyright (C) 2015 Reservoir Labs Inc., made open-source
+It was copyright (c) 2015 Reservoir Labs Inc., made open-source
 under the Gnu Public License (GPL), and published in a github repo.
 
 In 2021 and 2022, Andrew Appel and Ariel Kellison made contributions
diff --git a/doc/VCFloat-Manual.pdf b/doc/VCFloat-Manual.pdf
index b7864d9..29b984d 100644
Binary files a/doc/VCFloat-Manual.pdf and b/doc/VCFloat-Manual.pdf differ
diff --git a/doc/VCFloat-Manual.tex b/doc/VCFloat-Manual.tex
index 47e21bc..cb75b9b 100644
--- a/doc/VCFloat-Manual.tex
+++ b/doc/VCFloat-Manual.tex
@@ -102,6 +102,7 @@ \chapter{Introduction}
 \end{enumerate}
 
 \chapter{Floating-point functional models}
+\label{models}
 To use VCFloat you start with,
 \begin{lstlisting}
 Require Import vcfloat.VCFloat.
@@ -132,6 +133,7 @@ \chapter{Floating-point functional models}
 and \lstinline{1<24}, and so on.
 
 \chapter{NaNs}
+\label{NaNs}
 In the IEEE-754 floating-point standard, one cannot
 simply \emph{add} two numbers, one must specify how the NaNs will
 be propagated.  That is, if $x$ and $y$ are double-precision floats,
@@ -164,6 +166,7 @@ \chapter{NaNs}
 is never.
 
 \chapter{Notation Scopes}
+\label{notation}
 These notation scopes (and their delimiters) come with VCFloat:
 \begin{lstlisting}
 Delimit Scope float32_scope with F32.
@@ -181,6 +184,7 @@ \chapter{Notation Scopes}
 The variable $h$ is a double-precision floating-point number.
 
 \chapter{Operators}
+\label{operators}\label{models-last}
 The following operators are available in each notation scope:
 \begin{lstlisting}
   + $~$ - $~$ * $~$ / $~$ < $~$ <= $~$ > $~$ >= 
@@ -198,6 +202,7 @@ \chapter{Operators}
 
 
 \chapter{Example}
+\label{example}
 
 A mass on a spring---a harmonic oscillator---with position $x$ and
 velocity $v$ can be simulated over time-step $h=\frac{1}{32}$ using the
@@ -329,7 +334,7 @@ \chapter{Valmap and reflection}
 Definition step_vmap_list ($x$ $v$ : ftype Tsingle) := [(_x, existT ftype _ $x$);(_v, existT ftype _ $v$)].
 
 Definition step_vmap (x v : ftype Tsingle) : valmap :=
- ltac:(let z := compute_PTree (valmap_of_list (step_vmap_list x v)) in exact z).
+ ltac:(let z := ltac:(make_valmap_of_list (step_vmap_list x v))).
 \end{lstlisting}
 The auxiliary definition \lstinline{step_vmap_list}
 (when applied to $x$ and $v$)
@@ -356,6 +361,7 @@ \chapter{Valmap and reflection}
 the identity function.
 
 \chapter{Real-valued functional model}
+\label{realmodel}
 
 Suppose we take the float-valued functional model (the \lstinline{step}) 
 function) and interpret every constant and operator in the real numbers:
@@ -663,6 +669,7 @@ \chapter{prune\_terms}
 \end{lstlisting}
 in which not as many terms have been neglected.  But either way,
 \lstinline{interval} solves the goal.
+
 \chapter{error\_rewrites} Suppose an expression for the absolute
 forward error does not expand into a nice multinomial
 that is tractable for the \lstinline{prune_terms} tactic;
@@ -962,19 +969,302 @@ \chapter{Examples}
 \item[\href{../FPBench/}{FPBench/$*$.v}]  examples from the FPBench benchmark suite (fpbench.org)
 \end{description}
 
+\section{Nonstandard floating-point-like types}
+\label{nonstandard}
+
+Users may implement in software floating-point types that do not
+correspond exactly to any IEEE 754 format but that can be shown 
+to respect round-off error bounds. 
+VCFloat2 supports such user-defined types.
+
+Consider the example of double-double \cite{dekker71}.  A
+double-double number can be used to represent a
+floating-point number with at least 106 bits
+of mantissa using two double-precision floats whose 53-bit mantissas
+do not overlap (because their exponents differ by at least 53). One can add or multiply 
+numbers in this data type using just
+a few ordinary double-precision operations, especially on machines
+that support fused multiply-add (fma).
+
+The rounding behavior of double-double can be shown to be
+follow model with relative error $|\delta| \le 2^{-106}$ and
+absolute error $|\epsilon| \le 2^{-1022}$.
+If the user can prove such a property of an abstract number
+type (of which double-double is just one example), then they
+can build a \lstinline{nonstdtype} record in VCFloat2:
+
+\begin{lstlisting}
+Record nonstdtype 
+     (fprec: Z) (femax: Z) (prec_range: 1 < fprec < femax) := 
+ NONSTD 
+  { nonstd_rep: Type;
+    nonstd_to_F: nonstd_rep -> option (float radix2);
+    $\ldots$ (* some fields omitted *) $\ldots$
+    nonstd_bounds: forall x: nonstd_rep, 
+       ( - (bpow radix2 femax - bpow radix2 (femax - fprec)) <=
+        floatopt_to_real (nonstd_to_F x) <=
+        bpow radix2 femax - bpow radix2 (femax - fprec) )%R
+}.
+\end{lstlisting}
+Here, \lstinline{nonstd_bounds} is the user-supplied proof 
+of such a rounding theorem, \lstinline{nonstd_to_F}
+is the user-supplied definition of a function that maps 
+nonstandard types to a floating-point representation, and
+\lstinline{floatopt_to_real} is a function provided by
+VCFloat2 that maps  a floating-point representation to a real number. 
+
+After building a \lstinline{nonstdtype} record, the 
+ \lstinline{GTYPE} constructor can be used to build a new 
+VCFloat2 \lstinline{type}  (see Chapter~\ref{modeling}).
+Expressions in which some functions return
+values of this type and other functions take values of this type
+can now be reified, and VCFloat2 will automatically calculate
+and prove round-off error bounds.
+
+In order to write such expressions, users of VCFloat2 must first
+define operations on the newly defined \lstinline{type}. This
+is done by constructing a \lstinline{floatfunc} record
+(whose type was presented in Section~\ref{func}).
+
+\paragraph{Standard vs. nonstandard types.}  One might wonder what is
+special about a ``standard'' type, that it cannot be just an instance
+of the general notion of nonstandard type.  
+A standard type must support all the standard binary and unary operations
+(Zconst, BINOP, UNOP, PLUS, MINUS, $\ldots$ see Chapter~\ref{generic}).
+Nonstandard types support only whatever functions
+someone has supplied.  The notion of an arbitrary ``cast'' from
+any IEEE precision to any other cannot be generically supported,
+and (for example) some nonstandard types do not support Sterbenz
+subtraction, or constant literals.
+
+\chapter{Functional Modeling Languages}
+\label{modeling}
+
+VCFloat comes with (two variants of) a \emph{functional modeling language} for describing floating-point computations as functional programs.
+Chapters~\ref{models}--\ref{models-last} gave an informal introduction.   The modeling language(s) are useful not only for
+calling VCFloat's automated roundoff analysis but for other reasoning.
+
+The \emph{General} modeling language is VCFloat's default: it permits IEEE-754 floating-point types at any size of exponent and mantissa, as well as \emph{nonstandard} types such as flush-to-zero or double-double.  The \emph{Standard} modeling language permits only the IEEE-754 floating-point types at any size of exponent and mantissa; for some applications it is more convenient to use.
+
+\vfill
+\noindent\begin{tabular}{@{}l | p{2.4in}| p{2.4in} |@{}}
+\emph{Language} & \textbf{General} & \textbf{Standard} \\ \hline
+\emph{Purpose 1} & Ordinary use of VCFloat's automated roundoff calculations & (can be used, with conversion, for automated roundoff calculations) \\ \cline{2-3}
+\emph{Purpose 2} & Modeling computations that may involve nonstandard floats & Modeling computations using only IEEE floats \\ \cline{2-3}
+\emph{Advantage} & Generality & Easier conversion between \textsf{ftype(t)} and \textsf{binary\_float(fprec t)(femax t)} \\ \hline
+\emph{Semantics}
+& \begin{lstlisting}
+Record type: Type :=  
+    GTYPE {fprec: Z; femax: Z; $\ldots$; 
+        nonstd: option (nonstdtype $\ldots$)}.
+Definition TYPE fprecp femax $\ldots$ :=
+    GTYPE  fprecp femax $\ldots$ None.
+\end{lstlisting}
+& \begin{lstlisting}
+ Record type: Type :=
+    TYPE {fprec: Z; femax:Z, $\ldots$}
+\end{lstlisting} \\
+\hline
+\emph{Import} & \textsf{Require Import vcfloat.VCFloat.} & \textsf{From vcfloat\newline Require vcfloat.VCFloat.\newline Require Import vcfloat.FPStdLib.} \\ \hline
+\emph{Alt. Import} & \textsf{Require Import vcFloat.FPLib.} & \textsf{From vcfloat Require RAux FPStdLib.} \\
+& \multicolumn{2}{c|}{\emph{import this way when you don't need automatic roundoff calculation }} \\  \hline
+Alt. Import & & \textsf{Require Import vcfloat.FPStdLib.} \\
+&  & \emph{when you don't need much reasoning about how floats represent reals} \\
+\hline
+\end{tabular}
+\vfill
+
+\emph{Aside from} automatic roundoff calculations, both modeling languages come with several useful libraries for reasoning about floating-point:
+\begin{description}
+\item[Chapter~\ref{generic}:] Floating-point expressions that are generic over their precision, in an easier way than basic Flocq provides.
+\item[Chapter~\ref{notation}:] Notation systems for floating-point literals and expressions.
+\item[Chapter~\ref{morphisms}:] Equivalence relations on floating-point numbers, with Coq \emph{Morphisms} for automatic rewriting.
+\item[Chapter~\ref{conversions}:] Automatic generation of real-valued functional models from float-valued models.
+\end{description}
+
+\pagebreak
+
+\chapter{\emph{General} Modeling Language}
+
+The default functional modeling language in VCFloat is based on the notion of a floating-point format, called a \lstinline{type}:
+\begin{lstlisting}
+Record type: Type := GTYPE
+  { fprecp: positive;
+    femax: Z;
+    fprec := Z.pos fprecp;
+    fprec_lt_femax_bool: ZLT fprec femax;
+    fprecp_not_one_bool: Bool.Is_true (negb (Pos.eqb fprecp xH));
+    nonstd: option (nonstdtype fprecp femax fprec_lt_femax_bool fprecp_not_one_bool)
+  }.
+\end{lstlisting}
+The number \lstinline{fprec} is the number of bits in the matissa, \lstinline{femax} is the largest possible binary exponent.
+Propositions \lstinline{fprec_lt_femax_bool} and \lstinline{fprecp_not_one_bool} guarantee that $1 < \mathsf{fprec} < \mathsf{femax}$.
+Finally, \lstinline{nonstd} is None for an ordinary IEEE type (even of a nonstandard mantissa size or exponent size),
+and \lstinline{Some} for truly weird formats such as flush-to-zero\footnote{Some GPUs lack subnormal numbers, so instead of gradual underflow when one reaches the minimum (most negative) exponent, they round directly to zero.} or double-double.
+
+The constructor \lstinline{GTYPE} builds a \lstinline{type}, and the derived function \lstinline{TYPE} builds a standard type:
+
+\begin{lstlisting}
+Definition TYPE fprecp femax fprec_lt_femax fprecp_not_one :=
+    GTYPE  fprecp femax fprec_lt_femax fprecp_not_one None.
+
+Definition Tsingle := TYPE 24 128 I I.  (* IEEE 32-bit *)
+Definition Tdouble := TYPE 53 1024 I I. (* IEEE 64-bit *)
+\end{lstlisting}
+  
+Floating point numbers in format $t$ belong to (in Coq's type system) to \lstinline{ftype($t$)}.  One
+can convert between \lstinline{ftype($t$)} and the Flocq representation of IEEE types by using
+rewriting:
+
+\begin{lstlisting}
+Definition ftype: type -> Type := $\ldots$  
+
+Class is_standard ($t$: type) := 
+   Is_standard: match nonstd $t$ with None => True | _ => False end. 
+
+Definition ftype_of_float {$t$: type} {STD: is_standard $t$}:
+          binary_float (fprec $t$) (femax $t$) -> ftype $t$.
+
+Definition float_of_ftype {$t$: type} {STD: is_standard $t$}:
+          ftype $t$ -> binary_float (fprec $t$) (femax $t$).
+
+Lemma float_of_ftype_of_float {$t$: type} (STD1 STD2: is_standard $t$):
+  forall $x$, @float_of_ftype $t$ STD1 (@ftype_of_float $t$ STD2 $x$) = $x$.
+
+Lemma ftype_of_float_of_ftype {t: type} (STD1 STD2: is_standard t):
+  forall $x$, @ftype_of_float $t$ STD1 (@float_of_ftype $t$ STD2 $x$) = $x$.
+\end{lstlisting}
+
+In contrast, in the \emph{Standard} modeling language (described in the next chapter), 
+\lstinline{ftype $t$} is convertible with \lstinline{binary_float (fprec $t$) (femax $t$)}
+by \emph{unification}, without needing rewriting; this convenience is the main
+reason for having the Standard language.
+
+\chapter{\emph{Standard} Modeling Language}
+
+The nondefault ``Standard'' modeling language based on the notion of a floating-point format, called a \lstinline{type},
+but \emph{without a nonstd option}.
+
+The default functional modeling language in VCFloat is based on the notion of a floating-point format, called a \lstinline{type}:
+\begin{lstlisting}
+Record type: Type := TYPE
+  { fprecp: positive;
+    femax: Z;
+    fprec := Z.pos fprecp;
+    fprec_lt_femax_bool: ZLT fprec femax;
+    fprecp_not_one_bool: Bool.Is_true (negb (Pos.eqb fprecp xH))
+  }.
+
+Definition ftype ty := binary_float (fprec ty) (femax ty).
+
+Definition Tsingle := TYPE 24 128 I I.  (* IEEE 32-bit *)
+Definition Tdouble := TYPE 53 1024 I I. (* IEEE 64-bit *)
+\end{lstlisting}
+The number \lstinline{fprec} is the number of bits in the matissa, \lstinline{femax} is the largest possible binary exponent.  
+Clearly, \lstinline{ftype($t$)} is definitionally equal (hence unifiable) with 
+Flocq's  \lstinline{binary_float (fprec $t$) (femax $t$)}.
+
+One can \lstinline{Require} both modeling languages at once, but it is recommended not to \lstinline{Import} both at once,
+since they disagree about the meaning of \lstinline{type, ftype, Tsingle,} \emph{et cetera}.
+
+\chapter{Generic expressions}
+\label{generic}
+
+Consider the harmonic oscillator example shown in Chapter~\ref{example}.  That was given in single-precision floating point, but
+one could model the algorithm at arbitrary precision, and do proofs about it.  We would write,
+
+\begin{lstlisting}
+Require Import vcfloat.FPLib.
+Section WITHNANS.
+Context {NANS: Nans}.
+Definition h {t: type} `{STD: is_standard t} := BDIV (Zconst t 1) (Zconst t 32).
+Definition F {t: type} (x: ftype t)  `{STD: is_standard t} : ftype t := BMINUS (Zconst t 3) x.
+Definition step {t: type} `{STD: is_standard t}  (x v: ftype t) :=
+    BPLUS x (BMULT h (BPLUS v (BMULT (BDIV h (Zconst t 2)) (F x)))).
+End WITHNANS.
+\end{lstlisting}
+  
+Instead of importing FPLib (which gives access only to the ``General'' modeling language and morphisms)
+one could import all of vcfloat.VCFloat (which gives access in addition to the roundoff-error automation).
+However, roundoff-error automation works only at specific precisions; so after defining \lstinline{step}
+in this way, one could specialize it to \lstinline{@step Tsingle _} or \lstinline{@step Tdouble _}
+and call the automation.  However, there are many uses of VCFloat's supporting libraries
+even when its roundoff-error automation is not used.\footnote{Here are two examples.
+LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs, by Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel, 30th IEEE International Symposium on Computer Arithmetic, September 2023 (github.com/VeriNum/iterative\_methods).
+Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method, by Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, and Jean-Baptiste Jeannin, 16th Conference on Intelligent Computer Mathematics, September 2023 (github.com/VeriNum/LAProof).}
+
+If using FPStdLib instead of FPLib, to use the ``Standard'' modeling language,
+then omit the \lstinline{STD} arguments from the functions.
+
+\noindent\begin{tabular}{@{}l | p{2.9in}| p{2.0in} |@{}}
+  & \textbf{General} & \textbf{Standard} \\ \hline
+3 & \small \textsf{Zconst (t: type) `\{STD: is\_standard t\} (i: Z) : ftype t}
+  & \small \textsf{Zconst (t: type) (i: Z) : ftype t} \\ \hline
+  & \small \textsf{BINOP (op) (nan) \{t: type\} `\{STD: is\_standard t\}:\newline\hspace*{.4in} ftype t$\rightarrow$ftype t$\rightarrow$ftype t}
+  & \small \textsf{BINOP (op) (nan) \{t: type\}:\newline\hspace*{.4in}ftype t$\rightarrow$ftype t$\rightarrow$ftype t} \\
+$+$ & \small \textsf{BPLUS := BINOP Bplus plus\_nan} & \small \textsf{BPLUS := BINOP Bplus plus\_nan} \\
+$-$ & \small \textsf{BMINUS := BINOP Bminus minus\_nan} & \small \textsf{BMINUS := BINOP Bminus minus\_nan} \\ \hline
+  & \small \textsf{UNOP (op) (nan) \{t: type\} `\{STD: is\_standard t\}:\newline\hspace*{.4in} ftype t$\rightarrow$ftype t}
+  & \small \textsf{UNOP (op) (nan) \{t: type\}:\newline\hspace*{.4in} ftype t$\rightarrow$ftype t} \\
+
+$|\cdot |$ & \small \textsf{BABS \{t: type\} `\{STD: is\_standard t\}} & \small \textsf{BABS \{t: type\}} \\
+-  & \small \textsf{BOPP \{t: type\} `\{STD: is\_standard t\}} & \small \textsf{BOPP \{t: type\}} \\
+$\sqrt{~}$ & \small \textsf{BSQRT := UNOP Bsqrt sqrt\_nan} & \small \textsf{BSQRT := UNOP Bsqrt sqrt\_nan} \\ \hline
+$\_ \cdot \_ + \_$ & \small \textsf{BFMA} \emph{(fused multiply-add)} & \small \textsf{BFMA} \\ \hline
+& \multicolumn{2}{p{4.9in}|}{\small The \textsf{nan} parameter gives instructions on forming a NaN payload.  \textsf{BOPP,BABS}
+  cannot produce NaNs from non-NaNs, so do not need this parameter.} \\
+\end{tabular}
+
+\chapter{Equivalence relations and rewriting morphisms}
+\label{morphisms}
+
+When is the expression $a\cdot 0 + b$ equal to $b$?  This is important, for example, in modeling sparse matrix operations,
+where a dense representation computes the $a\cdot 0 + b$ where the sparse representation has simply $b$.
+
+Well, if $b=3.5$ and $a=\infty$ or $a=\mathrm{NaN}$, then $a\cdot 0 + b=\mathrm{NaN}$.  So we might ask, if $a$ and $b$ are known to be finite, is $a\cdot 0 + b$ equal to $b$?   And unfortunately, if $a$ is \emph{negative zero} and $b$ is \emph{positive zero}, then the fused-multiply-add $a\cdot 0 + b = -0$ while $b=+0$.
+
+This may be of little consequence when reasoning in the reals, where $-0 = +0$.  But often,
+in proving that a low-level implementation (in C or some other language) correctly implements a floating-point functional model,
+we want to avoid reasoning about the real-valued \emph{meaning} of the terms, and just treat floating-point operations
+as uninterpreted functions.  But even in that reasoning we want to consider $-0 \cong +0$.
+
+For this purpose, vcfloat.FPLib and vcfloat.FPStdLib (choose one) provide these relations:
+
+\begin{description}
+\item[$\mathsf{feq}~x~y$]    means that either $x$ and $y$ are both nonfinite (infinities or NaNs), or they are both zeros (regardless of sign), or they are identical.
+\item[$\mathsf{strict\_feq}~x~y$]    means $x$ and $y$ are both finite, and either they are both zeros (regardless of sign) or they are identical.  This is a \emph{partial equivalence relation} (or ``setoid'').
+\end{description}
+These relations are theorized in Coq's Setoid Morphism system, so you can use them in rewriting.  (There is a third relation,
+$mathsf{float_equiv}~x~y$,  meaning that either $x$ and $y$ are both NaNs or they are identical, which VCFloat uses internally but
+which is less useful for general purposes and is not theorized as a setoid.)
+
+For example, if $\mathsf{feq}~x~x' \land \mathsf{feq}~y~y' \land \mathsf{feq}~z~z'$ then
+$\mathsf{feq}~(x\cdot y + z)~(x'\cdot y' + z')$, and one can prove this easily by rewriting.
+
+\chapter{Conversions between models}
+\label{conversions}
+
+Given a floating-point functional model, one can convert it into the corresponding real-valued functional model
+by reifying and then using the \lstinline{rval} function, as described in Chapter~\ref{realmodel}.
+
+Given a model in the \emph{Standard} modeling language, one can automatically
+convert it into the \emph{Generic} modeling language using the \lstinline{type_coretype}
+relation.  But this is experimental and rather ill-documented.
+
 \chapter{Bibliography}
 
 \quad VCFloat 1.0 was built in 2015 and described in,\newline
 \textbf{A unified Coq framework for verifying C programs with floating-point computations}, by Tahina Ramananandro, Paul Mountcastle, Beno\^{\i}t  Meister, and Richard Lethin, in \emph{Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP'16)}, pages 15--26, 2016 (https://doi.org/10.1145/2854065.2854066).
 \vspace\baselineskip
 
-VCFloat 2.0 was built 2021-2022 and described in,\newline
+VCFloat 2.2 was built 2021-2023 and described in,\newline
 \textbf{VCFloat2: Floating-point error analysis in Coq},
 by Andrew W. Appel and Ariel E. Kellison,
-October 2022  (distributed as doc/vcfloat2.pdf in the vcfloat repo).
+in \emph{CPP'24: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+January 2024 (distributed as doc/vcfloat2.pdf in the vcfloat repo).
 \vspace\baselineskip
 
-VCFloat 2.0 is applied and demonstrated in,\newline
+VCFloat 2.0 was applied and demonstrated in,\newline
 \textbf{Verified numerical methods for ordinary differential equations},
 by Ariel E. Kellison and Andrew W. Appel,
 in \emph{15th International Workshop on Numerical Software Verification (NSV'22)}, August 2022.
diff --git a/vcfloat/.depend b/vcfloat/.depend
index 0afa1b2..b3578d7 100644
--- a/vcfloat/.depend
+++ b/vcfloat/.depend
@@ -18,6 +18,8 @@ FPLangOpt.vo FPLangOpt.glob FPLangOpt.v.beautified FPLangOpt.required_vo: FPLang
 FPLangOpt.vio: FPLangOpt.v Float_lemmas.vio FPLang.vio klist.vio LibTac.vio BigRAux.vio
 FPLib.vo FPLib.glob FPLib.v.beautified FPLib.required_vo: FPLib.v FPCore.vo RAux.vo Float_notations.vo
 FPLib.vio: FPLib.v FPCore.vio RAux.vio Float_notations.vio
+FPStdCompCert.vo FPStdCompCert.glob FPStdCompCert.v.beautified FPStdCompCert.required_vo: FPStdCompCert.v FPStdLib.vo FPCompCert.vo
+FPStdCompCert.vio: FPStdCompCert.v FPStdLib.vio FPCompCert.vio
 FPStdLib.vo FPStdLib.glob FPStdLib.v.beautified FPStdLib.required_vo: FPStdLib.v IEEE754_extra.vo klist.vo Float_notations.vo Base.vo FPCore.vo RAux.vo Rounding.vo
 FPStdLib.vio: FPStdLib.v IEEE754_extra.vio klist.vio Float_notations.vio Base.vio FPCore.vio RAux.vio Rounding.vio
 Float_lemmas.vo Float_lemmas.glob Float_lemmas.v.beautified Float_lemmas.required_vo: Float_lemmas.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo FPCore.vo
diff --git a/vcfloat/Automate.v b/vcfloat/Automate.v
index 216621b..3128932 100644
--- a/vcfloat/Automate.v
+++ b/vcfloat/Automate.v
@@ -1,6 +1,6 @@
-(** Automate.v:  proof automation for "ftype" usage-style of VCFloat.
- Copyright (C) 2021-2022 Andrew W. Appel.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
+
+(** Automate.v:  proof automation for "ftype" usage-style of VCFloat. *)
 
 Require Import Flocq.IEEE754.Binary.
 From vcfloat Require Import FPLang FPLangOpt RAux Rounding Reify Float_notations.
diff --git a/vcfloat/Base.v b/vcfloat/Base.v
index 3162766..e96f4cf 100644
--- a/vcfloat/Base.v
+++ b/vcfloat/Base.v
@@ -10,20 +10,19 @@ Lemma ZLT_intro a b:
   ZLT a b.
 Proof.
   intros.
-  apply Bool.Is_true_eq_left.
-  apply Z.ltb_lt.
-  assumption.
-Qed.
+  unfold ZLT, Bool.Is_true, Z.lt, Z.ltb in *.
+  rewrite H.
+  apply I.
+Defined.
 
 Lemma ZLT_elim a b:
   ZLT a b ->
   (a < b)%Z.
 Proof.
   intros.
-  apply Z.ltb_lt. 
-  apply Bool.Is_true_eq_true.
-  assumption.
-Qed.
+  unfold ZLT, Bool.Is_true, Z.lt, Z.ltb in *.
+  destruct (Z.compare a b); auto; contradiction.
+Defined.
 
 Lemma Is_true_eq a (h1 h2: Bool.Is_true a):
   h1 = h2.
diff --git a/vcfloat/BigQAux.v b/vcfloat/BigQAux.v
index d2a3790..679574a 100644
--- a/vcfloat/BigQAux.v
+++ b/vcfloat/BigQAux.v
@@ -1,36 +1,8 @@
-(** R-CoqLib: general-purpose Coq libraries and tactics.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of R-CoqLib, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole R-CoqLib library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
-Auxiliary theorems for big rational numbers
-*)
+(** R-CoqLib: general-purpose Coq libraries and tactics. *)
+
+(* Auxiliary theorems for big rational numbers *)
 
 Require Export Morphisms.
 Require Export QArith.
diff --git a/vcfloat/BigRAux.v b/vcfloat/BigRAux.v
index b244114..401368e 100644
--- a/vcfloat/BigRAux.v
+++ b/vcfloat/BigRAux.v
@@ -1,56 +1,6 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
-Auxiliary theorems for the real-number semantics of big rational
-numbers.
-*)
+(** Auxiliary theorems for the real-number semantics of big rational numbers. *)
 
 Require Export vcfloat.BigQAux.
 Require Export vcfloat.Q2RAux.
diff --git a/vcfloat/FPCompCert.v b/vcfloat/FPCompCert.v
index 34186e2..13161b4 100644
--- a/vcfloat/FPCompCert.v
+++ b/vcfloat/FPCompCert.v
@@ -1,57 +1,4 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-VCFloat: automatic translation of a CompCert Clight floating-point
-expression into a real-number expression with all rounding error terms
-and their correctness proofs.
-**)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
 Require Import Lia.
 From vcfloat Require Export FPCore. (* FPLang Rounding FPLangOpt.*)
diff --git a/vcfloat/FPCore.v b/vcfloat/FPCore.v
index c9cfc4d..f0574a2 100644
--- a/vcfloat/FPCore.v
+++ b/vcfloat/FPCore.v
@@ -1,44 +1,4 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 2.0 (2021-present)
- Copyright (C) 2023 Andrew W. Appel and Ariel E. Kellison
-
- Version 1.0 (2015-12-04) 
- Copyright (C) 2015 Reservoir Labs Inc.
- 
- Licensed by LGPL, see ../LICENSE
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
-
-    Version 2.0 is supported by the National Science Foundation
- grants 2219757 and 2219758.
-    Version 1.0 was sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following papers:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.  A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations. In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
-
- Andrew W. Appel and Ariel E. Kellison. VCFloat2: Floating-point Error 
- Analysis in Coq. April 2022.
-
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
 (** FPCore module.
   These definitions, which were previously part of FPLang.v, are 
diff --git a/vcfloat/FPLang.v b/vcfloat/FPLang.v
index baf328d..052fc2e 100644
--- a/vcfloat/FPLang.v
+++ b/vcfloat/FPLang.v
@@ -1,55 +1,6 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-VCFloat: core and annotated languages for floating-point operations.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
+
+(* Core and annotated languages for floating-point operations. *)
 
 Require Import Interval.Tactic.
 From vcfloat Require Export RAux.
diff --git a/vcfloat/FPLangOpt.v b/vcfloat/FPLangOpt.v
index 043458e..33ab652 100644
--- a/vcfloat/FPLangOpt.v
+++ b/vcfloat/FPLangOpt.v
@@ -1,55 +1,7 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-VCFloat: helpers for correct optimization of rounding error terms in
-the real-number semantics of floating-point computations.
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
+
+(** Helpers for correct optimization of rounding error terms in
+  the real-number semantics of floating-point computations.
 **)
 
 Require Export vcfloat.Float_lemmas.
diff --git a/vcfloat/FPStdCompCert.v b/vcfloat/FPStdCompCert.v
new file mode 100644
index 0000000..7c0cca7
--- /dev/null
+++ b/vcfloat/FPStdCompCert.v
@@ -0,0 +1,177 @@
+Require Import Lia.
+From vcfloat Require Import FPStdLib. (* FPLang Rounding FPLangOpt.*)
+Require compcert.common.AST compcert.common.Values.
+Require Import compcert.lib.Floats.
+Import Binary BinPos.
+
+Inductive val_inject: Values.val -> forall ty, ftype ty -> Prop :=
+| val_inject_single (f: ftype Tsingle):
+    val_inject (Values.Vsingle f) Tsingle f
+| val_inject_double f:
+    val_inject (Values.Vfloat f) Tdouble f
+.
+
+Lemma val_inject_single_inv (f1: float32) (f2: ftype Tsingle):
+  val_inject (Values.Vsingle f1) Tsingle f2 ->
+  f1 = f2.
+Proof.
+  inversion 1; subst.
+  apply ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.inj_pair2 in H2; auto.
+Qed.
+
+Lemma val_inject_double_inv f1 f2:
+  val_inject (Values.Vfloat f1) Tdouble f2 ->
+  f1 = f2.
+Proof.
+  inversion 1; subst.
+  apply ProofIrrelevance.ProofIrrelevanceTheory.EqdepTheory.inj_pair2 in H2; auto.
+Qed.
+
+Require vcfloat.FPCompCert.
+
+#[export] Instance nans: Nans := FPCompCert.nans.
+
+Lemma val_inject_eq_rect_r v ty1 e:
+  val_inject v ty1 e ->
+  forall ty2 (EQ: ty2 = ty1),
+    val_inject v ty2 (eq_rect_r _ e EQ).
+Proof.
+  intros.
+  subst.
+  assumption.
+Qed.
+      
+Lemma val_inject_single_inv_r v f:
+  val_inject v Tsingle f ->
+  v = Values.Vsingle f.
+Proof.
+  inversion 1; subst.
+  apply val_inject_single_inv in H.
+  congruence.
+Qed.
+
+Lemma val_inject_double_inv_r v f:
+  val_inject v Tdouble f ->
+  v = Values.Vfloat f.
+Proof.
+  inversion 1; subst.
+  apply val_inject_double_inv in H.
+  congruence.
+Qed.
+
+(** Why do we need this rewrite hint database?
+   You might think that all of this could be accomplished with "change"
+   instead of "rewrite".  But if you do that, then Qed takes forever. *)
+Lemma Float32_add_rewrite: Float32.add = @BPLUS _ Tsingle.
+Proof. reflexivity. Qed.
+
+#[export] Hint Rewrite Float32_add_rewrite : float_elim.
+Lemma Float32_sub_rewrite: Float32.sub = @BMINUS _ Tsingle.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float32_sub_rewrite : float_elim.
+Lemma Float32_mul_rewrite: Float32.mul = @BMULT _ Tsingle.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float32_mul_rewrite : float_elim.
+Lemma Float32_div_rewrite: Float32.div = @BDIV _ Tsingle.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float32_div_rewrite : float_elim.
+Lemma Float32_neg_rewrite: Float32.neg = @BOPP _ Tsingle.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float32_neg_rewrite : float_elim.
+Lemma Float32_abs_rewrite: Float32.abs = @BABS _ Tsingle.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float32_abs_rewrite : float_elim.
+
+Lemma Float_add_rewrite: Float.add = @BPLUS _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_add_rewrite : float_elim.
+Lemma Float_sub_rewrite: Float.sub = @BMINUS _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_sub_rewrite : float_elim.
+Lemma Float_mul_rewrite: Float.mul = @BMULT _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_mul_rewrite : float_elim.
+Lemma Float_div_rewrite: Float.div = @BDIV _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_div_rewrite : float_elim.
+Lemma Float_neg_rewrite: Float.neg = @BOPP _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_neg_rewrite : float_elim.
+Lemma Float_abs_rewrite: Float.abs = @BABS _ Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite Float_abs_rewrite : float_elim.
+
+Lemma float_of_single_eq: Float.of_single = @cast _ Tdouble Tsingle.
+Proof. reflexivity. Qed.
+
+Lemma float32_to_double_eq: Float32.to_double = @cast _ Tdouble Tsingle.
+Proof. reflexivity. Qed.
+Lemma float32_of_float_eq: Float32.of_double = @cast _ Tsingle Tdouble.
+Proof. reflexivity. Qed.
+Lemma float_to_single_eq: Float.to_single = @cast _ Tsingle Tdouble.
+Proof. reflexivity. Qed.
+#[export] Hint Rewrite float_of_single_eq float32_to_double_eq
+          float32_of_float_eq float_to_single_eq : float_elim.
+
+Import Float_notations.
+
+Lemma B754_finite_ext:
+  forall prec emax s m e p1 p2,
+    Binary.B754_finite prec emax s m e p1 = Binary.B754_finite prec emax s m e p2.
+Proof.
+intros.
+f_equal.
+apply Classical_Prop.proof_irrelevance.
+Qed.
+
+Import Integers.
+
+Ltac canonicalize_float_constant x :=
+match x with
+| Float32.of_bits (Int.repr ?a) =>
+  const_Z a;
+  let x' := constr:(Bits.b32_of_bits a) in
+  let y := eval compute in x' in
+ match y with
+   | Binary.B754_finite _ _ ?s ?m ?e _ =>
+     let z := constr:(b32_B754_finite s m e (@eq_refl bool true))
+      in change x with x'; 
+        replace x' with z by (apply B754_finite_ext; reflexivity)
+   | Binary.B754_zero _ _ ?s => 
+       let z := constr:(b32_B754_zero s) in
+       change x with z        
+  end
+| Float.of_bits (Int64.repr ?a) =>
+  const_Z a;
+  let x' := constr:(Bits.b64_of_bits a) in
+  let y := eval compute in x' in
+ match y with
+   | Binary.B754_finite _ _ ?s ?m ?e _ =>
+     let z := constr:(b64_B754_finite s m e (@eq_refl bool true))
+      in change x with x'; 
+        replace x' with z by (apply B754_finite_ext; reflexivity)
+   | Binary.B754_zero _ _ ?s => 
+       let z := constr:(b64_B754_zero s) in
+       change x with z        
+  end
+end.
+
+Ltac canonicalize_float_constants := 
+  repeat
+    match goal with
+    | |- context [Binary.B754_finite 24 128 ?s ?m ?e ?p] =>
+         let x := constr:(Binary.B754_finite 24 128 s m e p) in
+         let e' := eval compute in e in
+         let z := constr:(b32_B754_finite s m e' (@eq_refl bool true)) in
+         replace x with z by (apply B754_finite_ext; reflexivity)
+    | |- context [Binary.B754_finite 53 1024 ?s ?m ?e ?p] =>
+         let x := constr:(Binary.B754_finite 53 1024 s m e p) in
+         let e' := eval compute in e in
+         let z := constr:(b64_B754_finite s m e' (@eq_refl bool true)) in
+         replace x with z by (apply B754_finite_ext; reflexivity)
+    | |- context [Float32.of_bits (Int.repr ?a)] =>
+     canonicalize_float_constant constr:(Float32.of_bits (Int.repr a))
+    | |- context [Float.of_bits (Int64.repr ?a)] =>
+     canonicalize_float_constant constr:(Float.of_bits (Int64.repr a))
+    end.
+
diff --git a/vcfloat/FPStdLib.v b/vcfloat/FPStdLib.v
index a5308be..fbcbf3a 100644
--- a/vcfloat/FPStdLib.v
+++ b/vcfloat/FPStdLib.v
@@ -6,7 +6,7 @@ Global Unset Asymmetric Patterns. (* because "Require compcert..." sets it *)
 
 Require vcfloat.FPCore.
 
-From vcfloat Require Export RAux.
+From vcfloat Require Import RAux.
 Set Bullet Behavior "Strict Subproofs".
 Require Import Coq.Relations.Relations Coq.Classes.Morphisms Coq.Classes.RelationPairs Coq.Classes.RelationClasses.
 Require Import Coq.Lists.List.
@@ -189,6 +189,32 @@ Definition    fma_nan {NAN: Nans}:
         nan_payload (fprec ty) (femax ty)
  := fun t => @FPCore.fma_nan NAN (coretype_of_type t) _.
 
+Lemma fprec_gt_one ty:
+  (1 < fprec ty)%Z.
+Proof.
+  generalize (fprec_gt_0 ty).
+  unfold FLX.Prec_gt_0.
+  unfold fprec.
+  intros.
+  generalize (fprecp_not_one ty).
+  intros.
+  assert (Z.pos (fprecp ty) <> 1%Z) by congruence.
+  lia.
+Qed.
+
+
+Corollary any_nan ty: nan_payload (fprec ty) (femax ty).
+Proof.
+ red.
+  set (a:=1%positive).
+  assert (H: Binary.nan_pl (fprec ty) a = true).
+  unfold Binary.nan_pl.
+  subst a. 
+   pose proof (fprec_gt_one ty). simpl. lia.
+  exists (Binary.B754_nan (fprec ty) (femax ty) false 1 H).
+  reflexivity.
+Defined.
+
 
 Definition FT2R {t: type} : ftype t -> R := B2R (fprec t) (femax t).
 
@@ -434,19 +460,6 @@ Definition BINOP (op: ltac:( let t := type of Bplus in exact t ) )
     := op _ _ (fprec_gt_0 ty) (fprec_lt_femax ty) (op_nan ty)
       BinarySingleNaN.mode_NE.
 
-Lemma fprec_gt_one ty:
-  (1 < fprec ty)%Z.
-Proof.
-  generalize (fprec_gt_0 ty).
-  unfold FLX.Prec_gt_0.
-  unfold fprec.
-  intros.
-  generalize (fprecp_not_one ty).
-  intros.
-  assert (Z.pos (fprecp ty) <> 1%Z) by congruence.
-  lia.
-Qed.
-
 Section WITHNANS.
 Context {NANS: Nans}.
 
diff --git a/vcfloat/Float_lemmas.v b/vcfloat/Float_lemmas.v
index f43be41..b03126b 100644
--- a/vcfloat/Float_lemmas.v
+++ b/vcfloat/Float_lemmas.v
@@ -167,7 +167,7 @@ Definition fone: Defs.float Zaux.radix2 :=
     Defs.Fexp := 0
   |}.
 
-Open Scope R.
+Local Open Scope R_scope.
 
 Lemma F2R_fone: F2R _ fone = 1.
 Proof.
diff --git a/vcfloat/Fprop_absolute.v b/vcfloat/Fprop_absolute.v
index 9ecf79b..955f99b 100644
--- a/vcfloat/Fprop_absolute.v
+++ b/vcfloat/Fprop_absolute.v
@@ -1,56 +1,6 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
-More properties of floating-point numbers: absolute error,
-multiply/divide by radix.
-*)
+(** More properties of floating-point numbers: absolute error, multiply/divide by radix. *)
 
 Require Import ZArith Flocq.Core.Raux Reals.
 Require Import Lia Lra.
diff --git a/vcfloat/LibTac.v b/vcfloat/LibTac.v
index 5f934c3..95c7329 100644
--- a/vcfloat/LibTac.v
+++ b/vcfloat/LibTac.v
@@ -1,36 +1,7 @@
-(** R-CoqLib: general-purpose Coq libraries and tactics.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of R-CoqLib, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole R-CoqLib library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
-Basic tactics and logical properties.
-*)
+(** R-CoqLib: general-purpose Coq libraries and tactics. *)
+(** Basic tactics and logical properties. *)
 
 Ltac break K :=
   match type of K with
diff --git a/vcfloat/Makefile b/vcfloat/Makefile
index 7e11980..d2eb0ab 100644
--- a/vcfloat/Makefile
+++ b/vcfloat/Makefile
@@ -13,7 +13,7 @@ tests: ../Test/Test.vo ../Test/TestFunc.vo ../Test/TestPaper.vo ../Test/Test2.vo
 
 # the vcfloat2 target is the core VCFloat tool for VCFloat2 users who don't need
 # CompCert-based reification
-vcfloat2:  VCFloat.vo FPCompCert.vo Version.vo FPLib.vo FPStdLib.vo
+vcfloat2:  VCFloat.vo FPCompCert.vo Version.vo FPLib.vo FPStdLib.vo FPStdCompCert.vo
 
 %.vo: %.v
 	$(COQC) $(COQFLAGS) $*.v
diff --git a/vcfloat/Q2RAux.v b/vcfloat/Q2RAux.v
index e69271a..a83adf2 100644
--- a/vcfloat/Q2RAux.v
+++ b/vcfloat/Q2RAux.v
@@ -1,55 +1,5 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-Helpers for computing in rational numbers.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
+(* Helpers for computing in rational numbers. *)
 
 Require Export QArith Qreals Flocq.Core.Raux Reals.
 Open Scope R_scope.
diff --git a/vcfloat/RAux.v b/vcfloat/RAux.v
index 4a3129c..3e1a3bd 100644
--- a/vcfloat/RAux.v
+++ b/vcfloat/RAux.v
@@ -1,36 +1,5 @@
-(** R-CoqLib: general-purpose Coq libraries and tactics.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of R-CoqLib, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole R-CoqLib library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-More properties about real numbers.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
+(** More properties about real numbers. *)
 
 Require Export Reals Psatz.
 Require Export Lia.
diff --git a/vcfloat/Reify.v b/vcfloat/Reify.v
index 15d2390..8e260e7 100644
--- a/vcfloat/Reify.v
+++ b/vcfloat/Reify.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2022 Andrew W. Appel *)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
 From vcfloat Require Export RAux.
 From Flocq Require Import Binary Bits Core.
diff --git a/vcfloat/Rounding.v b/vcfloat/Rounding.v
index edfbccd..d6d4989 100644
--- a/vcfloat/Rounding.v
+++ b/vcfloat/Rounding.v
@@ -1,55 +1,4 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
-
-VCFloat: core and annotated languages for floating-point operations.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
 Require Import Interval.Tactic.
 From vcfloat Require Export RAux.
diff --git a/vcfloat/Summation.v b/vcfloat/Summation.v
index 698f871..8720cec 100644
--- a/vcfloat/Summation.v
+++ b/vcfloat/Summation.v
@@ -1,53 +1,6 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
-(**
-Author: Tahina Ramananandro <ramananandro@reservoir.com>
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 
+(**
 Accumulation of rounding errors for naive summation.
 
 For more technical information, you can read Section 5.4 of our paper
diff --git a/vcfloat/Version.v b/vcfloat/Version.v
index 375e8ea..b36cb27 100644
--- a/vcfloat/Version.v
+++ b/vcfloat/Version.v
@@ -1,2 +1,2 @@
 Require Import Coq.Strings.String.  Open Scope string.
-Definition version := "2.1".
+Definition version := "2.2".
diff --git a/vcfloat/junk/Example.v b/vcfloat/junk/Example.v
index c6ddbf9..125edb4 100644
--- a/vcfloat/junk/Example.v
+++ b/vcfloat/junk/Example.v
@@ -1,54 +1,8 @@
-(** VCFloat: A Unified Coq Framework for Verifying C Programs with
- Floating-Point Computations. Application to SAR Backprojection.
- 
- Version 1.0 (2015-12-04)
- 
- Copyright (C) 2015 Reservoir Labs Inc.
- All rights reserved.
- 
- This file, which is part of VCFloat, is free software. You can
- redistribute it and/or modify it under the terms of the GNU General
- Public License as published by the Free Software Foundation, either
- version 3 of the License (GNU GPL v3), or (at your option) any later
- version. A verbatim copy of the GNU GPL v3 is included in gpl-3.0.txt.
- 
- This file is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See LICENSE for
- more details about the use and redistribution of this file and the
- whole VCFloat library.
- 
- This work is sponsored in part by DARPA MTO as part of the Power
- Efficiency Revolution for Embedded Computing Technologies (PERFECT)
- program (issued by DARPA/CMO under Contract No: HR0011-12-C-0123). The
- views and conclusions contained in this work are those of the authors
- and should not be interpreted as representing the official policies,
- either expressly or implied, of the DARPA or the
- U.S. Government. Distribution Statement "A" (Approved for Public
- Release, Distribution Unlimited.)
- 
- 
- If you are using or modifying VCFloat in your work, please consider
- citing the following paper:
- 
- Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
- Lethin.
- A Unified Coq Framework for Verifying C Programs with Floating-Point
- Computations.
- In CPP (5th ACM/SIGPLAN conference on Certified Programs and Proofs)
- 2016.
- 
- 
- VCFloat requires third-party libraries listed in ACKS along with their
- copyright information.
- 
- VCFloat depends on third-party libraries listed in ACKS along with
- their copyright and licensing information.
-*)
+(*  LGPL licensed; see ../LICENSE and, for historical notes, see ../OLD_LICENSE *)
 (**
 Author: Tahina Ramananandro <ramananandro@reservoir.com>
 
-Examples from Section 4 of the abovementioned CPP 2016 paper.
+Examples from Section 4 of the CPP 2016 paper.
 **)
 
 Require Import Clight.