Skip to content

Commit

Permalink
Backport README and LICENSE changes from master branch
Browse files Browse the repository at this point in the history
  • Loading branch information
mattam82 committed Feb 15, 2018
1 parent d93f370 commit 33529a2
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 17 deletions.
4 changes: 3 additions & 1 deletion LICENSE
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
The MIT License (MIT)

Copyright (c) 2014 Gregory Malecha
Copyright (c) 2014-2018 Gregory Malecha
Copyright (c) 2015-2018 Abhishek Anand, Matthieu Sozeau
Copyright (c) 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
28 changes: 12 additions & 16 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ branch is in development and contains additional features:

- Example plugins built on top of this.

Documentation
=============

The 8.7 branch [documentation (coqdoc files)](html/Template.All.html)
and pretty-printed HTML versions of the [translations](html/translations) are available.

Papers
======

Expand All @@ -56,9 +62,12 @@ Contributors include [Yannick Forster](https://github.com/yforster),
[Cyril Cohen](https://github.com/CohenCyril) and [Nicolas
Tabareau](https://github.com/Tabareau).

(c) Copyright 2014-2018 Gregory Malecha\
(c) Copyright 2015-2018 Abhishek Anand, Matthieu Sozeau\
(c) Copyright 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 2014-2018 Gregory Malecha\
Copyright (c) 2015-2018 Abhishek Anand, Matthieu Sozeau\
Copyright (c) 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen

This software is distributed under the terms of the MIT license.
See [LICENSE](LICENSE) for details.

Branches
========
Expand Down Expand Up @@ -197,19 +206,6 @@ following code:
As long as you don't check this file into a repository things should work out
well.

Examples of plugins
-------------------
- a plugin to add a constructor in [test-suite/add_constructor.v](https://github.com/Template-Coq/template-coq/tree/coq-8.7/test-suite/add_constructor.v)
- a parametricity plugin in [translations/tsl_param.v](https://github.com/Template-Coq/template-coq/tree/coq-8.7/translations/tsl_param.v)
- a plugin to negate funext in [translations/fun.v](https://github.com/Template-Coq/template-coq/tree/coq-8.7/translations/tsl_fun.v)

Compile
-------
Use:
- `make` to compile the plugin
- `make translations` to compile the translation plugins
- `make test-suite` to compile the test suite

Bugs
====

Expand Down

0 comments on commit 33529a2

Please sign in to comment.