diff options
| author | Enrico Tassi | 2018-12-25 08:58:52 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-25 08:58:52 +0100 |
| commit | a92e4fbe88e16c312fe57a6f00ccba94322ee111 (patch) | |
| tree | 908036aba3e7aa68f8107f002cea0841047f37bc /plugins | |
| parent | b878216ca5e85f8164fa098b9dc0e688a212072d (diff) | |
[ssrmatching] update license banner (fix #9281)
This commit fixes a leftover of the merge of ssrmatching where
the .ml code received the appropriate banner, while the .v and
.mli di dnot.
Diffstat (limited to 'plugins')
| -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. |