diff options
author | 2016-01-21 16:45:23 +0100 | |
---|---|---|
committer | 2016-01-21 16:45:23 +0100 | |
commit | be0eca32fae93ed4793c2f839bb9e725b6a963d1 (patch) | |
tree | c2c5dce5ce24f5a2a8cade9e69410599c00e2b55 /plugins/decl_mode | |
parent | 9c2662eecc398f38be3b6280a8f760cc439bc31c (diff) | |
parent | 5e23fb90b39dfa014ae5c4fb46eb713cca09dbff (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/decl_mode')
-rw-r--r-- | plugins/decl_mode/decl_expr.mli | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_interp.mli | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_mode.mli | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 2 | ||||
-rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
-rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 2 |
9 files changed, 9 insertions, 9 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 3c4cacbc5..79ef3d186 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 1c56586ce..2a44dca21 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli index b3d6f82bd..4303ecdb4 100644 --- a/plugins/decl_mode/decl_interp.mli +++ b/plugins/decl_mode/decl_interp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 774c20c9a..acee3d6c2 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index fd7e15c15..dfeee833c 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 1741df533..f47b35541 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index f86bfea71..325969dad 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index d598e7c3f..b62cfd6ad 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index b3198dbf2..4c71f0410 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |