1. Remove obsolete license text; (2) tweak FPStdLib interface

1. Delete obsolete copyright notices (and related text) from many files.
These remained from VCFloat 1, and they no longer legally relevant
after the Qualcomm rights transfer of 2022.

2.  FPStdLib no longer Exports RAux, which means that users don't have
to do "Close Scope R_scope".

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

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

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.

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.

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 <[email protected]>
+(*  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.

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 <[email protected]>
+(*  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.

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 <[email protected]>
-
-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.*)

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 

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 <[email protected]>
-
-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.

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 <[email protected]>
-
-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.