From 54a7b862473fde07b4965eff2457e0a778bde42e 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:19:25 +0200 Subject: [PATCH] [wp/share] update headers --- src/plugins/wp/share/coqwp/BuiltIn.v | 3 ++- src/plugins/wp/share/coqwp/HighOrd.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/bool/Bool.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/int/Abs.v | 20 +++++++++---------- .../wp/share/coqwp/int/ComputerDivision.v | 20 +++++++++---------- .../wp/share/coqwp/int/Exponentiation.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/int/Int.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/int/MinMax.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/int/Power.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/map/Const.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/map/Map.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/Abs.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/ExpLog.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/FromInt.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/MinMax.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/PowerReal.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/Real.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/RealInfix.v | 20 +++++++++---------- src/plugins/wp/share/coqwp/real/Square.v | 20 +++++++++---------- .../wp/share/coqwp/real/Trigonometry.v | 20 +++++++++---------- src/plugins/wp/share/ergo/bool.Bool.mlw | 2 +- src/plugins/wp/share/ergo/int.Abs.mlw | 2 +- .../wp/share/ergo/int.ComputerDivision.mlw | 2 +- src/plugins/wp/share/ergo/int.Int.mlw | 2 +- src/plugins/wp/share/ergo/int.MinMax.mlw | 2 +- src/plugins/wp/share/ergo/map.Const.mlw | 2 +- src/plugins/wp/share/ergo/map.Map.mlw | 2 +- src/plugins/wp/share/ergo/real.Abs.mlw | 2 +- src/plugins/wp/share/ergo/real.ExpLog.mlw | 2 +- src/plugins/wp/share/ergo/real.FromInt.mlw | 2 +- src/plugins/wp/share/ergo/real.Hyperbolic.mlw | 2 +- src/plugins/wp/share/ergo/real.MinMax.mlw | 2 +- src/plugins/wp/share/ergo/real.Polar.mlw | 2 +- src/plugins/wp/share/ergo/real.PowerReal.mlw | 2 +- src/plugins/wp/share/ergo/real.Real.mlw | 2 +- src/plugins/wp/share/ergo/real.RealInfix.mlw | 2 +- src/plugins/wp/share/ergo/real.Square.mlw | 2 +- .../wp/share/ergo/real.Trigonometry.mlw | 2 +- src/plugins/wp/share/ergo/real.Truncate.mlw | 2 +- src/plugins/wp/share/src/alt_ergo_realize.ml | 2 +- .../wp/share/src/why3printer_realize.ml | 2 +- src/plugins/wp/why3_xml.mli | 2 +- src/plugins/wp/why3_xml.mll | 2 +- 43 files changed, 215 insertions(+), 214 deletions(-) diff --git a/src/plugins/wp/share/coqwp/BuiltIn.v b/src/plugins/wp/share/coqwp/BuiltIn.v index bd09b95be72..c7b225032cb 100644 --- a/src/plugins/wp/share/coqwp/BuiltIn.v +++ b/src/plugins/wp/share/coqwp/BuiltIn.v @@ -1,11 +1,12 @@ (**************************************************************************) (* *) (* 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. *) +(* *) (**************************************************************************) Require Export ZArith. diff --git a/src/plugins/wp/share/coqwp/HighOrd.v b/src/plugins/wp/share/coqwp/HighOrd.v index da42135acf8..4e75e9efbdb 100644 --- a/src/plugins/wp/share/coqwp/HighOrd.v +++ b/src/plugins/wp/share/coqwp/HighOrd.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) Require Import BuiltIn. diff --git a/src/plugins/wp/share/coqwp/bool/Bool.v b/src/plugins/wp/share/coqwp/bool/Bool.v index 9038682132e..826f424ce20 100644 --- a/src/plugins/wp/share/coqwp/bool/Bool.v +++ b/src/plugins/wp/share/coqwp/bool/Bool.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/Abs.v b/src/plugins/wp/share/coqwp/int/Abs.v index 5637e82b7da..b6fe3478d67 100644 --- a/src/plugins/wp/share/coqwp/int/Abs.v +++ b/src/plugins/wp/share/coqwp/int/Abs.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/ComputerDivision.v b/src/plugins/wp/share/coqwp/int/ComputerDivision.v index c34926e4c2f..060d4cdf041 100644 --- a/src/plugins/wp/share/coqwp/int/ComputerDivision.v +++ b/src/plugins/wp/share/coqwp/int/ComputerDivision.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/Exponentiation.v b/src/plugins/wp/share/coqwp/int/Exponentiation.v index f911f4cd6bd..0aa04b60e8e 100644 --- a/src/plugins/wp/share/coqwp/int/Exponentiation.v +++ b/src/plugins/wp/share/coqwp/int/Exponentiation.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/Int.v b/src/plugins/wp/share/coqwp/int/Int.v index a5106073930..8447e44455a 100644 --- a/src/plugins/wp/share/coqwp/int/Int.v +++ b/src/plugins/wp/share/coqwp/int/Int.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/MinMax.v b/src/plugins/wp/share/coqwp/int/MinMax.v index d969091e781..8510be57857 100644 --- a/src/plugins/wp/share/coqwp/int/MinMax.v +++ b/src/plugins/wp/share/coqwp/int/MinMax.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/int/Power.v b/src/plugins/wp/share/coqwp/int/Power.v index e2bed67ea5d..55d496108e2 100644 --- a/src/plugins/wp/share/coqwp/int/Power.v +++ b/src/plugins/wp/share/coqwp/int/Power.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/map/Const.v b/src/plugins/wp/share/coqwp/map/Const.v index c2ebf2444c8..51eddc01c4a 100644 --- a/src/plugins/wp/share/coqwp/map/Const.v +++ b/src/plugins/wp/share/coqwp/map/Const.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/map/Map.v b/src/plugins/wp/share/coqwp/map/Map.v index 1cb87d0a041..ac77830ba3f 100644 --- a/src/plugins/wp/share/coqwp/map/Map.v +++ b/src/plugins/wp/share/coqwp/map/Map.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/Abs.v b/src/plugins/wp/share/coqwp/real/Abs.v index 5c1bcd5b23d..33b579cdeaf 100644 --- a/src/plugins/wp/share/coqwp/real/Abs.v +++ b/src/plugins/wp/share/coqwp/real/Abs.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/ExpLog.v b/src/plugins/wp/share/coqwp/real/ExpLog.v index b0f17454da3..d666acbb9f2 100644 --- a/src/plugins/wp/share/coqwp/real/ExpLog.v +++ b/src/plugins/wp/share/coqwp/real/ExpLog.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/FromInt.v b/src/plugins/wp/share/coqwp/real/FromInt.v index fa6f14fc385..5d61bbdfdd2 100644 --- a/src/plugins/wp/share/coqwp/real/FromInt.v +++ b/src/plugins/wp/share/coqwp/real/FromInt.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/MinMax.v b/src/plugins/wp/share/coqwp/real/MinMax.v index 3f6ade0b9ac..deccab540b9 100644 --- a/src/plugins/wp/share/coqwp/real/MinMax.v +++ b/src/plugins/wp/share/coqwp/real/MinMax.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/PowerReal.v b/src/plugins/wp/share/coqwp/real/PowerReal.v index 1532b405d1b..15404bf4e75 100644 --- a/src/plugins/wp/share/coqwp/real/PowerReal.v +++ b/src/plugins/wp/share/coqwp/real/PowerReal.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/Real.v b/src/plugins/wp/share/coqwp/real/Real.v index 8fc9927ec9b..eca3f8f8ea4 100644 --- a/src/plugins/wp/share/coqwp/real/Real.v +++ b/src/plugins/wp/share/coqwp/real/Real.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/RealInfix.v b/src/plugins/wp/share/coqwp/real/RealInfix.v index fe99b70efc6..af4165dc282 100644 --- a/src/plugins/wp/share/coqwp/real/RealInfix.v +++ b/src/plugins/wp/share/coqwp/real/RealInfix.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/Square.v b/src/plugins/wp/share/coqwp/real/Square.v index 11e34192e34..dd62746a2d5 100644 --- a/src/plugins/wp/share/coqwp/real/Square.v +++ b/src/plugins/wp/share/coqwp/real/Square.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/coqwp/real/Trigonometry.v b/src/plugins/wp/share/coqwp/real/Trigonometry.v index 04707511fb3..4fb4e404c1f 100644 --- a/src/plugins/wp/share/coqwp/real/Trigonometry.v +++ b/src/plugins/wp/share/coqwp/real/Trigonometry.v @@ -1,13 +1,13 @@ -(********************************************************************) -(* *) -(* The Why3 Verification Platform / The Why3 Development Team *) -(* 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. *) -(* *) -(********************************************************************) +(**************************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* 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. *) +(* *) +(**************************************************************************) (* This file is generated by Why3's Coq-realize driver *) (* Beware! Only edit allowed sections below *) diff --git a/src/plugins/wp/share/ergo/bool.Bool.mlw b/src/plugins/wp/share/ergo/bool.Bool.mlw index bb1399469ab..e31c6ffa0dc 100644 --- a/src/plugins/wp/share/ergo/bool.Bool.mlw +++ b/src/plugins/wp/share/ergo/bool.Bool.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/int.Abs.mlw b/src/plugins/wp/share/ergo/int.Abs.mlw index bfaf4a42bb2..e03de293a71 100644 --- a/src/plugins/wp/share/ergo/int.Abs.mlw +++ b/src/plugins/wp/share/ergo/int.Abs.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/int.ComputerDivision.mlw b/src/plugins/wp/share/ergo/int.ComputerDivision.mlw index b6f17a3e97a..743d5fa35a3 100644 --- a/src/plugins/wp/share/ergo/int.ComputerDivision.mlw +++ b/src/plugins/wp/share/ergo/int.ComputerDivision.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/int.Int.mlw b/src/plugins/wp/share/ergo/int.Int.mlw index c5821cb8432..703c83034f6 100644 --- a/src/plugins/wp/share/ergo/int.Int.mlw +++ b/src/plugins/wp/share/ergo/int.Int.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/int.MinMax.mlw b/src/plugins/wp/share/ergo/int.MinMax.mlw index 6dff092e7d8..5bbc63f7812 100644 --- a/src/plugins/wp/share/ergo/int.MinMax.mlw +++ b/src/plugins/wp/share/ergo/int.MinMax.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/map.Const.mlw b/src/plugins/wp/share/ergo/map.Const.mlw index eb73c12af2a..eb7f9a8995d 100644 --- a/src/plugins/wp/share/ergo/map.Const.mlw +++ b/src/plugins/wp/share/ergo/map.Const.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/map.Map.mlw b/src/plugins/wp/share/ergo/map.Map.mlw index 56ddd1ea93d..ddb3b00ec7e 100644 --- a/src/plugins/wp/share/ergo/map.Map.mlw +++ b/src/plugins/wp/share/ergo/map.Map.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Abs.mlw b/src/plugins/wp/share/ergo/real.Abs.mlw index 24664ffe802..1340bfad895 100644 --- a/src/plugins/wp/share/ergo/real.Abs.mlw +++ b/src/plugins/wp/share/ergo/real.Abs.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.ExpLog.mlw b/src/plugins/wp/share/ergo/real.ExpLog.mlw index 05dd26a4905..a600122dfd8 100644 --- a/src/plugins/wp/share/ergo/real.ExpLog.mlw +++ b/src/plugins/wp/share/ergo/real.ExpLog.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.FromInt.mlw b/src/plugins/wp/share/ergo/real.FromInt.mlw index fc67bc41a88..6c0d9c52160 100644 --- a/src/plugins/wp/share/ergo/real.FromInt.mlw +++ b/src/plugins/wp/share/ergo/real.FromInt.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Hyperbolic.mlw b/src/plugins/wp/share/ergo/real.Hyperbolic.mlw index daa086fd265..da5f26b3c17 100644 --- a/src/plugins/wp/share/ergo/real.Hyperbolic.mlw +++ b/src/plugins/wp/share/ergo/real.Hyperbolic.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.MinMax.mlw b/src/plugins/wp/share/ergo/real.MinMax.mlw index e4d32828a64..d1438d67fd2 100644 --- a/src/plugins/wp/share/ergo/real.MinMax.mlw +++ b/src/plugins/wp/share/ergo/real.MinMax.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Polar.mlw b/src/plugins/wp/share/ergo/real.Polar.mlw index 48c14d709ef..4c953665ad7 100644 --- a/src/plugins/wp/share/ergo/real.Polar.mlw +++ b/src/plugins/wp/share/ergo/real.Polar.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.PowerReal.mlw b/src/plugins/wp/share/ergo/real.PowerReal.mlw index b0d583f3b79..8e5923d76a8 100644 --- a/src/plugins/wp/share/ergo/real.PowerReal.mlw +++ b/src/plugins/wp/share/ergo/real.PowerReal.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Real.mlw b/src/plugins/wp/share/ergo/real.Real.mlw index cf6ffb24db6..db80917b1b0 100644 --- a/src/plugins/wp/share/ergo/real.Real.mlw +++ b/src/plugins/wp/share/ergo/real.Real.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.RealInfix.mlw b/src/plugins/wp/share/ergo/real.RealInfix.mlw index 3b5f00b1623..5134839728a 100644 --- a/src/plugins/wp/share/ergo/real.RealInfix.mlw +++ b/src/plugins/wp/share/ergo/real.RealInfix.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Square.mlw b/src/plugins/wp/share/ergo/real.Square.mlw index c4f1fcbf01f..4eaec010938 100644 --- a/src/plugins/wp/share/ergo/real.Square.mlw +++ b/src/plugins/wp/share/ergo/real.Square.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Trigonometry.mlw b/src/plugins/wp/share/ergo/real.Trigonometry.mlw index fac0a529cad..bd5fa3953ae 100644 --- a/src/plugins/wp/share/ergo/real.Trigonometry.mlw +++ b/src/plugins/wp/share/ergo/real.Trigonometry.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/ergo/real.Truncate.mlw b/src/plugins/wp/share/ergo/real.Truncate.mlw index e963d526cf4..f86ba0df6fb 100644 --- a/src/plugins/wp/share/ergo/real.Truncate.mlw +++ b/src/plugins/wp/share/ergo/real.Truncate.mlw @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/src/alt_ergo_realize.ml b/src/plugins/wp/share/src/alt_ergo_realize.ml index 2d62d57d54f..31bd1ce3ff9 100644 --- a/src/plugins/wp/share/src/alt_ergo_realize.ml +++ b/src/plugins/wp/share/src/alt_ergo_realize.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/share/src/why3printer_realize.ml b/src/plugins/wp/share/src/why3printer_realize.ml index a65ee6812bc..6042541b3fc 100644 --- a/src/plugins/wp/share/src/why3printer_realize.ml +++ b/src/plugins/wp/share/src/why3printer_realize.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/why3_xml.mli b/src/plugins/wp/why3_xml.mli index b2c124a3cd4..788c602b990 100644 --- a/src/plugins/wp/why3_xml.mli +++ b/src/plugins/wp/why3_xml.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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/src/plugins/wp/why3_xml.mll b/src/plugins/wp/why3_xml.mll index a65a587f62a..f178197c0d6 100644 --- a/src/plugins/wp/why3_xml.mll +++ b/src/plugins/wp/why3_xml.mll @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* 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 *) -- GitLab