Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package flocq for openSUSE:Factory checked in at 2023-09-20 13:25:46 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/flocq (Old) and /work/SRC/openSUSE:Factory/.flocq.new.16627 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "flocq" Wed Sep 20 13:25:46 2023 rev:6 rq:1111804 version:4.1.3 Changes: -------- --- /work/SRC/openSUSE:Factory/flocq/flocq.changes 2023-03-29 23:28:40.111927850 +0200 +++ /work/SRC/openSUSE:Factory/.flocq.new.16627/flocq.changes 2023-09-20 13:27:32.543104655 +0200 @@ -1,0 +2,8 @@ +Sun Sep 17 18:49:04 UTC 2023 - Aaron Puchert <[email protected]> + +- Update to version 4.1.2. + * Ensured compatibility from Coq 8.12 to 8.18. +- Update to version 4.1.3. + * Avoided breaking users of `IEEE754.PrimFloat`. + +------------------------------------------------------------------- Old: ---- flocq-4.1.1.tar.gz New: ---- flocq-4.1.3.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ flocq.spec ++++++ --- /var/tmp/diff_new_pack.a8bA69/_old 2023-09-20 13:27:34.119161118 +0200 +++ /var/tmp/diff_new_pack.a8bA69/_new 2023-09-20 13:27:34.119161118 +0200 @@ -19,7 +19,7 @@ Name: flocq -Version: 4.1.1 +Version: 4.1.3 Release: 0 Summary: Formalization of floating point numbers for Coq Group: Productivity/Scientific/Math @@ -66,11 +66,15 @@ # Make the documentation point to coq-doc if possible. grep "\-\-coqlib_url http://coq.inria.fr/distrib/current/stdlib"; Remakefile.in && +%if %{pkg_vcmp coq >= 8.18} +sed -i "s|--coqlib_url http://coq.inria.fr/distrib/current/stdlib|--coqlib %{_libdir}/coq --coqlib_url %{_defaultdocdir}/coq/stdlib|" Remakefile.in +%else %if %{pkg_vcmp coq >= 8.14} sed -i "s|--coqlib_url http://coq.inria.fr/distrib/current/stdlib|--coqlib %{_libdir}/coq-core --coqlib_url %{_defaultdocdir}/coq/stdlib|" Remakefile.in %else sed -i "s|--coqlib_url http://coq.inria.fr/distrib/current/stdlib|--coqlib %{_libdir}/coq-core|" Remakefile.in %endif +%endif %build # This is not autotools-compatible, so we don't use the macro. ++++++ flocq-4.1.1.tar.gz -> flocq-4.1.3.tar.gz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/NEWS.md new/flocq-4.1.3/NEWS.md --- old/flocq-4.1.1/NEWS.md 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/NEWS.md 2023-09-08 10:13:39.000000000 +0200 @@ -1,3 +1,13 @@ +Version 4.1.3 +------------- + +* avoided breaking users of `IEEE754.PrimFloat` + +Version 4.1.2 +------------- + +* ensured compatibility from Coq 8.12 to 8.18 + Version 4.1.1 ------------- diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/README.md new/flocq-4.1.3/README.md --- old/flocq-4.1.1/README.md 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/README.md 2023-09-08 10:13:39.000000000 +0200 @@ -8,7 +8,7 @@ PROJECT HOME ------------ -Homepage: http://flocq.gforge.inria.fr/ +Homepage: https://flocq.gitlabpages.inria.fr/ Repository: https://gitlab.inria.fr/flocq/flocq diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/Remakefile.in new/flocq-4.1.3/Remakefile.in --- old/flocq-4.1.1/Remakefile.in 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/Remakefile.in 2023-09-08 10:13:39.000000000 +0200 @@ -35,6 +35,7 @@ IEEE754/PrimFloat.v \ Pff/Pff.v \ Pff/Pff2FlocqAux.v \ + @NAT2Z_FILE@ \ Pff/Pff2Flocq.v OBJS = $(addprefix src/,$(addsuffix o,$(FILES))) @@ -63,7 +64,7 @@ check-more: $(MOBJS) -CONFIGURED_FILES = Remakefile src/Version.v src/IEEE754/Int63Compat.v +CONFIGURED_FILES = Remakefile src/Version.v src/IEEE754/Int63Compat.v src/Pff/Nat2Z_compat.v $(CONFIGURED_FILES): %: %.in config.status ./config.status $@ @@ -72,7 +73,7 @@ autoconf ./config.status --recheck -%.vo: %.v | src/IEEE754/Int63Compat.v +%.vo: %.v | src/IEEE754/Int63Compat.v src/Pff/Nat2Z_compat.v @COQDEP@ -R src Flocq $< | @REMAKE@ -r $@ @COQC@ @COQEXTRAFLAGS@ -q -R src Flocq $< diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/configure new/flocq-4.1.3/configure --- old/flocq-4.1.1/configure 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/configure 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.71 for Flocq 4.1.1. +# Generated by GNU Autoconf 2.71 for Flocq 4.1.3. # # Report bugs to <Sylvie Boldo <[email protected]>, Guillaume Melquiond <[email protected]>>. # @@ -671,8 +671,8 @@ # Identity of this package. PACKAGE_NAME='Flocq' PACKAGE_TARNAME='flocq' -PACKAGE_VERSION='4.1.1' -PACKAGE_STRING='Flocq 4.1.1' +PACKAGE_VERSION='4.1.3' +PACKAGE_STRING='Flocq 4.1.3' PACKAGE_BUGREPORT='Sylvie Boldo <[email protected]>, Guillaume Melquiond <[email protected]>' PACKAGE_URL='' @@ -690,6 +690,8 @@ COQEXTRAFLAGS COQDOC COQDEP +NAT2Z_FILE +NAT2Z_EXPORT INT63_FILE INT63_EXPORT COQC @@ -1305,7 +1307,7 @@ # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF -\`configure' configures Flocq 4.1.1 to adapt to many kinds of systems. +\`configure' configures Flocq 4.1.3 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1367,7 +1369,7 @@ if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of Flocq 4.1.1:";; + short | recursive ) echo "Configuration of Flocq 4.1.3:";; esac cat <<\_ACEOF @@ -1456,7 +1458,7 @@ test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -Flocq configure 4.1.1 +Flocq configure 4.1.3 generated by GNU Autoconf 2.71 Copyright (C) 2021 Free Software Foundation, Inc. @@ -1532,7 +1534,7 @@ This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by Flocq $as_me 4.1.1, which was +It was created by Flocq $as_me 4.1.3, which was generated by GNU Autoconf 2.71. Invocation command line was $ $0$ac_configure_args_raw @@ -2135,13 +2137,19 @@ case $? in #( 1) : INT63_EXPORT="From Coq Require Export Int63." - INT63_FILE="" ;; #( + INT63_FILE="" + NAT2Z_EXPORT="Require Export Nat2Z_8_12." + NAT2Z_FILE="Pff/Nat2Z_8_12.v" ;; #( 0) : INT63_EXPORT="Require Export Int63Copy." - INT63_FILE="IEEE754/Int63Copy.v" ;; #( + INT63_FILE="IEEE754/Int63Copy.v" + NAT2Z_EXPORT="" + NAT2Z_FILE="" ;; #( 2) : INT63_EXPORT="Require Export Int63Copy." - INT63_FILE="IEEE754/Int63Copy.v" ;; #( + INT63_FILE="IEEE754/Int63Copy.v" + NAT2Z_EXPORT="" + NAT2Z_FILE="" ;; #( *) : ;; esac @@ -2149,6 +2157,8 @@ + + { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for coqdep" >&5 printf %s "checking for coqdep... " >&6; } if test ! "$COQDEP"; then @@ -2839,7 +2849,7 @@ esac fi -ac_config_files="$ac_config_files Remakefile src/Version.v src/IEEE754/Int63Compat.v" +ac_config_files="$ac_config_files Remakefile src/Version.v src/IEEE754/Int63Compat.v src/Pff/Nat2Z_compat.v" cat >confcache <<\_ACEOF # This file is a shell script that caches the results of configure @@ -3376,7 +3386,7 @@ # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by Flocq $as_me 4.1.1, which was +This file was extended by Flocq $as_me 4.1.3, which was generated by GNU Autoconf 2.71. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -3431,7 +3441,7 @@ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_config='$ac_cs_config_escaped' ac_cs_version="\\ -Flocq config.status 4.1.1 +Flocq config.status 4.1.3 configured by $0, generated by GNU Autoconf 2.71, with options \\"\$ac_cs_config\\" @@ -3544,6 +3554,7 @@ "Remakefile") CONFIG_FILES="$CONFIG_FILES Remakefile" ;; "src/Version.v") CONFIG_FILES="$CONFIG_FILES src/Version.v" ;; "src/IEEE754/Int63Compat.v") CONFIG_FILES="$CONFIG_FILES src/IEEE754/Int63Compat.v" ;; + "src/Pff/Nat2Z_compat.v") CONFIG_FILES="$CONFIG_FILES src/Pff/Nat2Z_compat.v" ;; *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;; esac diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/configure.in new/flocq-4.1.3/configure.in --- old/flocq-4.1.1/configure.in 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/configure.in 2023-09-08 10:13:39.000000000 +0200 @@ -1,4 +1,4 @@ -AC_INIT([Flocq], [4.1.1], +AC_INIT([Flocq], [4.1.3], [Sylvie Boldo <[email protected]>, Guillaume Melquiond <[email protected]>], [flocq]) @@ -32,11 +32,17 @@ AX_VERSION_GE([$coq_version], 8.14, [INT63_EXPORT="Require Export Int63Copy." - INT63_FILE="IEEE754/Int63Copy.v"], + INT63_FILE="IEEE754/Int63Copy.v" + NAT2Z_EXPORT="" + NAT2Z_FILE=""], [INT63_EXPORT="From Coq Require Export Int63." - INT63_FILE=""]) + INT63_FILE="" + NAT2Z_EXPORT="Require Export Nat2Z_8_12." + NAT2Z_FILE="Pff/Nat2Z_8_12.v"]) AC_SUBST(INT63_EXPORT) AC_SUBST(INT63_FILE) +AC_SUBST(NAT2Z_EXPORT) +AC_SUBST(NAT2Z_FILE) AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]]) AC_MSG_CHECKING([for coqdep]) @@ -87,5 +93,5 @@ esac fi -AC_CONFIG_FILES([Remakefile src/Version.v src/IEEE754/Int63Compat.v]) +AC_CONFIG_FILES([Remakefile src/Version.v src/IEEE754/Int63Compat.v src/Pff/Nat2Z_compat.v]) AC_OUTPUT diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Average.v new/flocq-4.1.3/examples/Average.v --- old/flocq-4.1.1/examples/Average.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Average.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Sylvie Boldo diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Cody_Waite.v new/flocq-4.1.3/examples/Cody_Waite.v --- old/flocq-4.1.1/examples/Cody_Waite.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Cody_Waite.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Guillaume Melquiond diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Compute.v new/flocq-4.1.3/examples/Compute.v --- old/flocq-4.1.1/examples/Compute.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Compute.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2015-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Division_u16.v new/flocq-4.1.3/examples/Division_u16.v --- old/flocq-4.1.1/examples/Division_u16.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Division_u16.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Guillaume Melquiond diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Double_rounding_odd_radix.v new/flocq-4.1.3/examples/Double_rounding_odd_radix.v --- old/flocq-4.1.1/examples/Double_rounding_odd_radix.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Double_rounding_odd_radix.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Pierre Roux diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Homogen.v new/flocq-4.1.3/examples/Homogen.v --- old/flocq-4.1.1/examples/Homogen.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Homogen.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2016-2018 Guillaume Melquiond diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Print17.v new/flocq-4.1.3/examples/Print17.v --- old/flocq-4.1.1/examples/Print17.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Print17.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2021 Pierre Roux diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Sqrt_sqr.v new/flocq-4.1.3/examples/Sqrt_sqr.v --- old/flocq-4.1.1/examples/Sqrt_sqr.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Sqrt_sqr.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2013-2018 Sylvie Boldo diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/examples/Triangle.v new/flocq-4.1.3/examples/Triangle.v --- old/flocq-4.1.1/examples/Triangle.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/examples/Triangle.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This example is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Sylvie Boldo diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Bracket.v new/flocq-4.1.3/src/Calc/Bracket.v --- old/flocq-4.1.1/src/Calc/Bracket.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Bracket.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># @@ -651,7 +651,7 @@ now apply Z_mod_lt. rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_IZR. rewrite Zmult_comm, Zplus_assoc. -now rewrite <- Z_div_mod_eq. +(try now rewrite <- Z_div_mod_eq_full); now rewrite <- Z_div_mod_eq. (* remove the try and the second part when requiring Coq >= 8.14 *) Qed. Theorem inbetween_float_new_location_single : diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Div.v new/flocq-4.1.3/src/Calc/Div.v --- old/flocq-4.1.1/src/Calc/Div.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Div.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Operations.v new/flocq-4.1.3/src/Calc/Operations.v --- old/flocq-4.1.1/src/Calc/Operations.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Operations.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Plus.v new/flocq-4.1.3/src/Calc/Plus.v --- old/flocq-4.1.1/src/Calc/Plus.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Plus.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2021 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Round.v new/flocq-4.1.3/src/Calc/Round.v --- old/flocq-4.1.1/src/Calc/Round.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Round.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Calc/Sqrt.v new/flocq-4.1.3/src/Calc/Sqrt.v --- old/flocq-4.1.1/src/Calc/Sqrt.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Calc/Sqrt.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Core.v new/flocq-4.1.3/src/Core/Core.v --- old/flocq-4.1.1/src/Core/Core.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Core.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Defs.v new/flocq-4.1.3/src/Core/Defs.v --- old/flocq-4.1.1/src/Core/Defs.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Defs.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Digits.v new/flocq-4.1.3/src/Core/Digits.v --- old/flocq-4.1.1/src/Core/Digits.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Digits.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2011-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/FIX.v new/flocq-4.1.3/src/Core/FIX.v --- old/flocq-4.1.1/src/Core/FIX.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/FIX.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/FLT.v new/flocq-4.1.3/src/Core/FLT.v --- old/flocq-4.1.1/src/Core/FLT.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/FLT.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/FLX.v new/flocq-4.1.3/src/Core/FLX.v --- old/flocq-4.1.1/src/Core/FLX.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/FLX.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/FTZ.v new/flocq-4.1.3/src/Core/FTZ.v --- old/flocq-4.1.1/src/Core/FTZ.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/FTZ.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Float_prop.v new/flocq-4.1.3/src/Core/Float_prop.v --- old/flocq-4.1.1/src/Core/Float_prop.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Float_prop.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Generic_fmt.v new/flocq-4.1.3/src/Core/Generic_fmt.v --- old/flocq-4.1.1/src/Core/Generic_fmt.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Generic_fmt.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Raux.v new/flocq-4.1.3/src/Core/Raux.v --- old/flocq-4.1.1/src/Core/Raux.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Raux.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Round_NE.v new/flocq-4.1.3/src/Core/Round_NE.v --- old/flocq-4.1.1/src/Core/Round_NE.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Round_NE.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Round_pred.v new/flocq-4.1.3/src/Core/Round_pred.v --- old/flocq-4.1.1/src/Core/Round_pred.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Round_pred.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Ulp.v new/flocq-4.1.3/src/Core/Ulp.v --- old/flocq-4.1.1/src/Core/Ulp.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Ulp.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2009-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Core/Zaux.v new/flocq-4.1.3/src/Core/Zaux.v --- old/flocq-4.1.1/src/Core/Zaux.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Core/Zaux.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2011-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/IEEE754/Binary.v new/flocq-4.1.3/src/IEEE754/Binary.v --- old/flocq-4.1.1/src/IEEE754/Binary.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/IEEE754/Binary.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/IEEE754/BinarySingleNaN.v new/flocq-4.1.3/src/IEEE754/BinarySingleNaN.v --- old/flocq-4.1.1/src/IEEE754/BinarySingleNaN.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/IEEE754/BinarySingleNaN.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/IEEE754/Bits.v new/flocq-4.1.3/src/IEEE754/Bits.v --- old/flocq-4.1.1/src/IEEE754/Bits.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/IEEE754/Bits.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2011-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/IEEE754/PrimFloat.v new/flocq-4.1.3/src/IEEE754/PrimFloat.v --- old/flocq-4.1.1/src/IEEE754/PrimFloat.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/IEEE754/PrimFloat.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2018-2019 Guillaume Bertholon #<br /># @@ -25,6 +25,29 @@ From Coq Require Import ZArith Reals Floats SpecFloat. Require Import Zaux BinarySingleNaN. +(* Compatibility workaround, remove once requiring Coq >= 8.15 *) +Module Import Compat. +Definition ldexp f (_ : Z) : float := f. +Definition frexp (f : float) := (f, Z0). +End Compat. +Import FloatOps. +Module Import Z. +Notation ldexp := ldexp. +Notation frexp := frexp. +End Z. +Import Floats. +Import Zaux BinarySingleNaN. + +(* Compatibility workaround, remove once requiring Coq >= 8.15 *) +Lemma Z_ldexp_spec f e : + Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e. +Proof. try exact (Z_ldexp_spec f e); exact (ldexp_spec f e). Qed. + +(* Compatibility workaround, remove once requiring Coq >= 8.15 *) +Lemma Z_frexp_spec f : + let (m, e) := Z.frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f). +Proof. try exact (Z_frexp_spec f); exact (frexp_spec f). Qed. + (** Conversions from/to Flocq binary_float *) Definition Prim2B (x : float) : binary_float prec emax := @@ -268,14 +291,14 @@ Theorem ldexp_equiv : forall x e, - Prim2B (ldexp x e) = Bldexp mode_NE (Prim2B x) e. + Prim2B (Z.ldexp x e) = Bldexp mode_NE (Prim2B x) e. Proof. intros x e. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. -rewrite ldexp_spec. +rewrite Z_ldexp_spec. rewrite <-!B2SF_Prim2B. case (Prim2B x) as [sx|sx| |sx mx ex Bx]; [now trivial.. | ]. simpl. @@ -302,12 +325,12 @@ Theorem frexp_equiv : forall x : float, - let (m, e) := frexp x in + let (m, e) := Z.frexp x in (Prim2B m, e) = Bfrexp (Prim2B x). Proof. intro x. -generalize (frexp_spec x). -destruct frexp as [f e]. +generalize (Z_frexp_spec x). +destruct Z.frexp as [f e]. rewrite <-(B2SF_Prim2B x). replace (SFfrexp _ _ _) with (let (f, e) := Bfrexp (Prim2B x) in @@ -329,7 +352,7 @@ Proof. intro x. generalize (frexp_equiv x). -unfold frexp. +unfold Z.frexp. now case frshiftexp. Qed. @@ -361,7 +384,7 @@ unfold ulp, Bulp'. rewrite one_equiv, ldexp_equiv, Prim2B_B2Prim. generalize (frexp_equiv x). -case frexp; intros f e. +case Z.frexp; intros f e. destruct Bfrexp as [f' e']. now intros [= _ <-]. Qed. @@ -378,15 +401,15 @@ rewrite <-B2SF_Prim2B. assert (Hsndfrexp : forall x : binary_float prec emax, snd (SFfrexp prec emax (B2SF x)) = snd (Bfrexp x)). { intro x'. - generalize (frexp_spec (B2Prim x')). + generalize (Z_frexp_spec (B2Prim x')). generalize (frexp_equiv (B2Prim x')). - case frexp; intros f' e'. + case Z.frexp; intros f' e'. rewrite Prim2B_B2Prim, Prim2SF_B2Prim. intros H H'; generalize (f_equal snd H'); generalize (f_equal snd H); simpl. now intros ->. } assert (Hldexp : forall x e, SFldexp prec emax (B2SF x) e = B2SF (Bldexp mode_NE x e)). { intros x' e'. - rewrite <-(Prim2B_B2Prim x'), B2SF_Prim2B, <-ldexp_spec. + rewrite <-(Prim2B_B2Prim x'), B2SF_Prim2B, <-Z_ldexp_spec. now rewrite <-B2SF_Prim2B, ldexp_equiv. } assert (Hulp : forall x, SFulp prec emax (B2SF x) = B2SF (Bulp' x)). { intro x'. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Pff/Nat2Z_8_12.v new/flocq-4.1.3/src/Pff/Nat2Z_8_12.v --- old/flocq-4.1.1/src/Pff/Nat2Z_8_12.v 1970-01-01 01:00:00.000000000 +0100 +++ new/flocq-4.1.3/src/Pff/Nat2Z_8_12.v 2023-09-08 10:13:39.000000000 +0200 @@ -0,0 +1,12 @@ +Require Import ZArith. + +Module Nat2Z. + +Notation inj_lt := Nat2Z.inj_lt. +Notation inj_le := Nat2Z.inj_le. +Notation inj := Nat2Z.inj. + +Lemma inj_div n m : Z.of_nat (n / m) = (Z.of_nat n / Z.of_nat m)%Z. +Proof. now case m; [case n|intro m'; apply div_Zdiv]. Qed. + +End Nat2Z. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Pff/Nat2Z_compat.v.in new/flocq-4.1.3/src/Pff/Nat2Z_compat.v.in --- old/flocq-4.1.1/src/Pff/Nat2Z_compat.v.in 1970-01-01 01:00:00.000000000 +0100 +++ new/flocq-4.1.3/src/Pff/Nat2Z_compat.v.in 2023-09-08 10:13:39.000000000 +0200 @@ -0,0 +1,6 @@ +(* Generated from Nat2Z_compat.v.in, *do not edit*. *) + +(* This is a compatibility module for Coq < 8.14. + It is bound to disappear once Flocq requires Coq >= 8.14. *) + +@NAT2Z_EXPORT@ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Pff/Pff2Flocq.v new/flocq-4.1.3/src/Pff/Pff2Flocq.v --- old/flocq-4.1.1/src/Pff/Pff2Flocq.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Pff/Pff2Flocq.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2016-2018 Sylvie Boldo #<br /># @@ -21,6 +21,7 @@ Require Import Core Plus_error Mult_error Operations Sterbenz. Require Import Pff Pff2FlocqAux. +Require Import Nat2Z_compat. (* remove when requiring Coq >= 8.14 *) Open Scope R_scope. @@ -899,9 +900,8 @@ assert (Hs:(s =(Z.abs_nat prec - Nat.div2 (Z.abs_nat prec))%nat)). unfold s; rewrite inj_minus. assert (TT: (Z.div2 prec = Nat.div2 (Z.abs_nat prec))%Z). -rewrite Nat.div2_div, Z.div2_div, div_Zdiv; simpl. +rewrite Nat.div2_div, Z.div2_div, Nat2Z.inj_div; simpl. rewrite inj_abs; lia. -lia. rewrite <- TT. rewrite inj_abs; try lia. rewrite Z.max_r; try lia. diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Pff/Pff2FlocqAux.v new/flocq-4.1.3/src/Pff/Pff2FlocqAux.v --- old/flocq-4.1.1/src/Pff/Pff2FlocqAux.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Pff/Pff2FlocqAux.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2013-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Div_sqrt_error.v new/flocq-4.1.3/src/Prop/Div_sqrt_error.v --- old/flocq-4.1.1/src/Prop/Div_sqrt_error.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Div_sqrt_error.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Double_rounding.v new/flocq-4.1.3/src/Prop/Double_rounding.v --- old/flocq-4.1.1/src/Prop/Double_rounding.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Double_rounding.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2014-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Mult_error.v new/flocq-4.1.3/src/Prop/Mult_error.v --- old/flocq-4.1.1/src/Prop/Mult_error.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Mult_error.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Plus_error.v new/flocq-4.1.3/src/Prop/Plus_error.v --- old/flocq-4.1.1/src/Prop/Plus_error.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Plus_error.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Relative.v new/flocq-4.1.3/src/Prop/Relative.v --- old/flocq-4.1.1/src/Prop/Relative.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Relative.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Round_odd.v new/flocq-4.1.3/src/Prop/Round_odd.v --- old/flocq-4.1.1/src/Prop/Round_odd.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Round_odd.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2013-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Prop/Sterbenz.v new/flocq-4.1.3/src/Prop/Sterbenz.v --- old/flocq-4.1.1/src/Prop/Sterbenz.v 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Prop/Sterbenz.v 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2010-2018 Sylvie Boldo #<br /># diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/flocq-4.1.1/src/Version.v.in new/flocq-4.1.3/src/Version.v.in --- old/flocq-4.1.1/src/Version.v.in 2023-02-24 16:37:25.000000000 +0100 +++ new/flocq-4.1.3/src/Version.v.in 2023-09-08 10:13:39.000000000 +0200 @@ -1,6 +1,6 @@ (** This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ +arithmetic in Coq: https://flocq.gitlabpages.inria.fr/ Copyright (C) 2011-2018 Sylvie Boldo #<br />#
