diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/Omega.v | 10 | ||||
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 16 | ||||
| -rw-r--r-- | plugins/omega/OmegaPlugin.v | 10 | ||||
| -rw-r--r-- | plugins/omega/OmegaTactic.v | 10 | ||||
| -rw-r--r-- | plugins/omega/PreOmega.v | 10 | ||||
| -rw-r--r-- | plugins/omega/coq_omega.ml | 10 | ||||
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 10 | ||||
| -rw-r--r-- | plugins/omega/omega.ml | 10 |
8 files changed, 51 insertions, 35 deletions
diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index a53a38d35..6c8f23a01 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**************************************************************************) (* *) diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index 1872f5766..dc86a9899 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) Require Import BinInt Znat. Local Open Scope Z_scope. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index ce187892d..3c339c8b8 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* To strictly import the omega tactic *) diff --git a/plugins/omega/OmegaTactic.v b/plugins/omega/OmegaTactic.v index ce187892d..3c339c8b8 100644 --- a/plugins/omega/OmegaTactic.v +++ b/plugins/omega/OmegaTactic.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* To strictly import the omega tactic *) diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 93103e026..59fd9b801 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Arith Max Min BinInt BinNat Znat Nnat. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4271c80cd..51cd665f6 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**************************************************************************) (* *) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index f7b153a13..170b937c9 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**************************************************************************) (* *) diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 6a1efe85b..2510c1693 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**************************************************************************) (* *) |