diff options
| author | Maxime Dénès | 2019-01-08 09:59:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-08 09:59:09 +0100 |
| commit | 727d4da625f88b7ba302d5c129f9773dc1fb1e33 (patch) | |
| tree | 9ff05b1a07354ebf20a76c065a14370343280aaf | |
| parent | d6fe12b3ce8299a161c59ff8ed0657531af70329 (diff) | |
| parent | a92e4fbe88e16c312fe57a6f00ccba94322ee111 (diff) | |
Merge PR #9282: [ssrmatching] update license banner (fix #9281)
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 11 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.v | 12 |
2 files changed, 21 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f0bb6f58a6..ff2c900130 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,5 +1,14 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) open Goal open Environ diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 9a53e1dd1a..a39f76db9e 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -1,5 +1,15 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) + Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. |