diff --git a/src/plugins/wp/share/coqwp/BuiltIn.v b/src/plugins/wp/share/coqwp/BuiltIn.v index bd09b95be72e13a5a840e6baa8ca140d9805ecdc..c7b225032cbc6eedc8072332692b66d1f4c313ab 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 da42135acf8f61280beecc37296a761f70134ca4..4e75e9efbdb316ceeffb7d5dcf5a94ed714a5af1 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 9038682132e398aa54c4168348f364db9f7e1ac0..826f424ce2013b9a8ac4247b2b7e911b5ab1366f 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 5637e82b7dacbce17a776dae26afeca3dc0c4333..b6fe3478d67cf158b4cf8a934417d199445d4253 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 c34926e4c2fcdd44c6a8e2fb11e18be5241f24dd..060d4cdf041e7b48a4519df08b21a0caf220e572 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 f911f4cd6bda205689f287c4c3a9398140ba9c9e..0aa04b60e8e6b576f2bdec2e10caf6c317d726b8 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 a5106073930d4a7cafe8d7f84883d0756b28c832..8447e44455a8811f74a165299a52a74483c10e9d 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 d969091e7810e422f58e80b10c076bc2d5f09704..8510be57857c24211f5f5e364c706e612bf78bed 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 e2bed67ea5dd8ad31ec00b8246b77e12cffe93e1..55d496108e2c03e74cffffcce5bec06abb2253ec 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 c2ebf2444c87bc8a7a8f6c5d337b1b734b94bfd5..51eddc01c4ae4b66d6ed9fac2a60a9392fc3696b 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 1cb87d0a041491c37ebdebdbfe6eb8f18cd6fc80..ac77830ba3f8a85d6480b75f5cefb4ff1e3eddad 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 5c1bcd5b23db2c13c4d14a1543ed94a10052c27c..33b579cdeaf8b5725b3225e9b50e36f8427112d1 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 b0f17454da3d2b1f126611525f6944dcafff82bb..d666acbb9f2112960790b95888e27b0e8e288d84 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 fa6f14fc3853322f7b041c4000e060f29c0ffb92..5d61bbdfdd2cc73243cf83f791b1fcbf4267db2b 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 3f6ade0b9ac3f6e71d3ac798c720e26860ecd962..deccab540b9680049daae23ec9f46ba05f0b6d7f 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 1532b405d1b6e16e368ad34b05abdba7b3a57f9b..15404bf4e7590a876e7fd9d5412f5e58f12f98d6 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 8fc9927ec9bfdc1a5356e288542103a6a648ab17..eca3f8f8ea4d724e2a1eae2291a2759168a9f68a 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 fe99b70efc6e17dae668c46566b6fbeaef60cab2..af4165dc28272360516d75f42fe15c8c7a32135c 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 11e34192e345ec8fc325f139ef8b8b8b5b417115..dd62746a2d5153d35276ce60103ba0f1d336c758 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 04707511fb389e17dcf319e6334d970374f631e4..4fb4e404c1f9a324321c9927fa621f799e40fd6f 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 bb1399469ab1dbbd59291fac687bc5faa304ba3f..e31c6ffa0dcbc70040a4db98b637938760e52c21 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 bfaf4a42bb2c0f354ee235a756c5f80d6524725c..e03de293a7104e962c3d046e2a4b4c47fb57d572 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 b6f17a3e97abdc550572c3aa6b7222ed7bd5d4b1..743d5fa35a3cf70f041690f79611f24057e4e55d 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 c5821cb8432b2e8140e881a1d6ed051cb942aeac..703c83034f641fe81a193048411fb921648182a2 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 6dff092e7d8eb18e75094f693427f72ca7939c1a..5bbc63f78125e8a2f8ae673961a740e801b59582 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 eb73c12af2a86426c968aab8ec5f7766a0adc617..eb7f9a8995df727f3a0b11ed847a20bfbc05a92d 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 56ddd1ea93d2ed2a336aea6fe5571bcd5e0315c6..ddb3b00ec7e09e5b1bafa89f4421e2a37b6ee0ec 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 24664ffe802ac893c7ea75bfe2df4cf8f3d11a8d..1340bfad895cf643a707f95e455b6a88b6fd81a2 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 05dd26a4905b0f588013e0cafdb6b782057e0b83..a600122dfd8185e26c6f1dba6dddfa3decfdb20b 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 fc67bc41a88b7012c62f5a6c21f1766eca257392..6c0d9c52160f4d452bed86a6f3eb130600d91ef8 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 daa086fd265d7ef3890ff2b0133b3406c06ece63..da5f26b3c17adf34b5b8db48c585f8d682645c93 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 e4d32828a648a9ebcf82cdbf6aacda186c12f3a4..d1438d67fd2d8b51cba1a8b2f74db3b65b34ec99 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 48c14d709ef77ea65aad401abf891ae784f648e1..4c953665ad72a84b9b036919327f73bd00a52a2a 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 b0d583f3b798f3190eac1f627cb2a8d839317ad1..8e5923d76a87a4d9e99339a82bf110f60ac2aa6b 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 cf6ffb24db6ac2315970b1ccde8db7c8aa382104..db80917b1b0b39d54729ec9c3b07a8bbf451311c 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 3b5f00b16236b6607cb51303738716b8db0840c8..5134839728aff4c170354cdb4d709da7418a7bcf 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 c4f1fcbf01f494c38057667f0b7738e92782e71b..4eaec010938bcd45adf0fd9894486a36232fcaf9 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 fac0a529cad52be1364481e5b42ff2d315817214..bd5fa3953ae28867e5ba5555fecc499c09be93cd 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 e963d526cf4c44b3aead210d699aef4af2c6685f..f86ba0df6fb6717d8d4f9ab7d7182db95c9af023 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 2d62d57d54fec07432f3321e25b2edf40393e5c8..31bd1ce3ff9afaf68b65cf30bb84b0e97486d2eb 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 a65ee6812bc55410f04e2d028402da1fd8cf6999..6042541b3fc9aadd9ac0c2365725d1ceb6d255a5 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 b2c124a3cd4491636a6f5faa56d58f34f3214809..788c602b9904b9d52a668e32c9ff9225c4d72246 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 a65a587f62a8ec74fa11e266ae62924ff158ab8c..f178197c0d62c4e680731ddc588344a11c43fe3f 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 *)