adam@517: "Certified Programming with Dependent Types" code license information adam@517: adam@517: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ adam@517: adam@517: CAUTION: Most of the source files in this distribution are NOT adam@517: open-source in the usual sense. See the comment at the beginning of adam@517: each source file for its license, which is Creative Commons, oriented adam@517: more toward free distribution of books than the usual collaborative adam@517: model of open-source software. The author really is trying to keep adam@517: you from remixing your own versions of the book, which MIT Press might adam@517: not be too happy about. adam@517: adam@517: However, a few of the library modules used here are sufficiently adam@517: useful that they are released separately under a BSD license, included adam@517: below. The author wants to repeat some advice from the book text, adam@517: though: please don't use these library modules in real projects. They adam@517: are not designed for any use beside getting the reader up and running adam@517: quickly in reading the book. All of their content, including the adam@517: "crush" functionality, is rather trivial to implement from scratch for adam@517: your own projects, using the techniques that the book presents. adam@517: adam@517: adam@517: The following license applies ONLY to the source files: adam@517: CpdtTactics.v adam@517: MoreSpecif.v adam@517: DepList.v adam@517: adam@517: ~~~~~~~~~~~ adam@517: BSD LICENSE adam@517: ~~~~~~~~~~~ adam@517: adam@517: Copyright (c) 2006-2013, Adam Chlipala adam@517: All rights reserved. adam@517: adam@517: Redistribution and use in source and binary forms, with or without adam@517: modification, are permitted provided that the following conditions are met: adam@517: adam@517: - Redistributions of source code must retain the above copyright notice, adam@517: this list of conditions and the following disclaimer. adam@517: - Redistributions in binary form must reproduce the above copyright notice, adam@517: this list of conditions and the following disclaimer in the documentation adam@517: and/or other materials provided with the distribution. adam@517: - The names of contributors may not be used to endorse or promote products adam@517: derived from this software without specific prior written permission. adam@517: adam@517: THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adam@517: AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adam@517: IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adam@517: ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adam@517: LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adam@517: CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adam@517: SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adam@517: INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adam@517: CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adam@517: ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adam@517: POSSIBILITY OF SUCH DAMAGE.