From 5c5c6dcaad820cb087491cfa3faf6032c18b30fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Fri, 19 Apr 2019 18:13:29 +0200 Subject: [PATCH] [wp/share] fix headers specs --- headers/close-source/MODIFIED_WHY3 | 2 +- headers/close-source/UNMODIFIED_WHY3 | 3 ++- headers/header_spec.txt | 3 +++ headers/open-source/MODIFIED_WHY3 | 2 +- headers/open-source/UNMODIFIED_WHY3 | 3 ++- 5 files changed, 9 insertions(+), 4 deletions(-) diff --git a/headers/close-source/MODIFIED_WHY3 b/headers/close-source/MODIFIED_WHY3 index a3af4fb4e56..8a26d2f1814 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 5d86a7e0f00..aa2704bc4d6 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 c60f329e2a1..349e71dd3c5 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 a3af4fb4e56..8a26d2f1814 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 5d86a7e0f00..aa2704bc4d6 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. + -- GitLab