Skip to content

Commit 33529a2

Browse files
committed
Backport README and LICENSE changes from master branch
1 parent d93f370 commit 33529a2

File tree

2 files changed

+15
-17
lines changed

2 files changed

+15
-17
lines changed

LICENSE

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
The MIT License (MIT)
22

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

57
Permission is hereby granted, free of charge, to any person obtaining a copy
68
of this software and associated documentation files (the "Software"), to deal

README.md

Lines changed: 12 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,12 @@ branch is in development and contains additional features:
3333

3434
- Example plugins built on top of this.
3535

36+
Documentation
37+
=============
38+
39+
The 8.7 branch [documentation (coqdoc files)](html/Template.All.html)
40+
and pretty-printed HTML versions of the [translations](html/translations) are available.
41+
3642
Papers
3743
======
3844

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

59-
(c) Copyright 2014-2018 Gregory Malecha\
60-
(c) Copyright 2015-2018 Abhishek Anand, Matthieu Sozeau\
61-
(c) Copyright 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen
65+
Copyright (c) 2014-2018 Gregory Malecha\
66+
Copyright (c) 2015-2018 Abhishek Anand, Matthieu Sozeau\
67+
Copyright (c) 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen
68+
69+
This software is distributed under the terms of the MIT license.
70+
See [LICENSE](LICENSE) for details.
6271

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

200-
Examples of plugins
201-
-------------------
202-
- 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)
203-
- a parametricity plugin in [translations/tsl_param.v](https://github.com/Template-Coq/template-coq/tree/coq-8.7/translations/tsl_param.v)
204-
- a plugin to negate funext in [translations/fun.v](https://github.com/Template-Coq/template-coq/tree/coq-8.7/translations/tsl_fun.v)
205-
206-
Compile
207-
-------
208-
Use:
209-
- `make` to compile the plugin
210-
- `make translations` to compile the translation plugins
211-
- `make test-suite` to compile the test suite
212-
213209
Bugs
214210
====
215211

0 commit comments

Comments
 (0)