diff --git a/headers/close-source/MODIFIED_WHY3 b/headers/close-source/MODIFIED_WHY3 index a3af4fb4e569fc238f81f1b6981c08c659cd9c2d..8a26d2f1814d45492a65cf0ebf53fadd3d9addb6 100644 --- a/headers/close-source/MODIFIED_WHY3 +++ b/headers/close-source/MODIFIED_WHY3 @@ -1,6 +1,6 @@ The Why3 Verification Platform / The Why3 Development Team -Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University +Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University This software is distributed under the terms of the GNU Lesser General Public License version 2.1, with the special exception diff --git a/headers/close-source/UNMODIFIED_WHY3 b/headers/close-source/UNMODIFIED_WHY3 index 5d86a7e0f0035a76c9b9e0c5ce125608594ce15a..aa2704bc4d608128bdc9fe4d0a7fd00542aae960 100644 --- a/headers/close-source/UNMODIFIED_WHY3 +++ b/headers/close-source/UNMODIFIED_WHY3 @@ -1,7 +1,8 @@ The Why3 Verification Platform / The Why3 Development Team -Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University +Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University This software is distributed under the terms of the GNU Lesser General Public License version 2.1, with the special exception on linking described in file LICENSE. + diff --git a/headers/header_spec.txt b/headers/header_spec.txt index c60f329e2a1fa61190aa06a7722a339ac9887b2a..349e71dd3c508bd4bdcc0acf59f407e9657a3491 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1799,6 +1799,7 @@ src/plugins/wp/share/coqwp/Cfloat.v: CEA_WP src/plugins/wp/share/coqwp/Cint.v: CEA_WP src/plugins/wp/share/coqwp/Cmath.v: CEA_WP src/plugins/wp/share/coqwp/ExpLog.v: CEA_WP +src/plugins/wp/share/coqwp/HighOrd.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/Memory.v: CEA_WP src/plugins/wp/share/coqwp/Qed.v: CEA_WP src/plugins/wp/share/coqwp/Qedlib.v: CEA_WP @@ -1809,8 +1810,10 @@ src/plugins/wp/share/coqwp/Zbits.v: CEA_WP src/plugins/wp/share/coqwp/bool/Bool.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/int/Abs.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/int/ComputerDivision.v: UNMODIFIED_WHY3 +src/plugins/wp/share/coqwp/int/Exponentiation.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/int/Int.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/int/MinMax.v: UNMODIFIED_WHY3 +src/plugins/wp/share/coqwp/int/Power.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/map/Map.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/map/Const.v: UNMODIFIED_WHY3 src/plugins/wp/share/coqwp/real/Abs.v: UNMODIFIED_WHY3 diff --git a/headers/open-source/MODIFIED_WHY3 b/headers/open-source/MODIFIED_WHY3 index a3af4fb4e569fc238f81f1b6981c08c659cd9c2d..8a26d2f1814d45492a65cf0ebf53fadd3d9addb6 100644 --- a/headers/open-source/MODIFIED_WHY3 +++ b/headers/open-source/MODIFIED_WHY3 @@ -1,6 +1,6 @@ The Why3 Verification Platform / The Why3 Development Team -Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University +Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University This software is distributed under the terms of the GNU Lesser General Public License version 2.1, with the special exception diff --git a/headers/open-source/UNMODIFIED_WHY3 b/headers/open-source/UNMODIFIED_WHY3 index 5d86a7e0f0035a76c9b9e0c5ce125608594ce15a..aa2704bc4d608128bdc9fe4d0a7fd00542aae960 100644 --- a/headers/open-source/UNMODIFIED_WHY3 +++ b/headers/open-source/UNMODIFIED_WHY3 @@ -1,7 +1,8 @@ The Why3 Verification Platform / The Why3 Development Team -Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University +Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University This software is distributed under the terms of the GNU Lesser General Public License version 2.1, with the special exception on linking described in file LICENSE. +