Commit Graph

5 Commits

Author SHA1 Message Date
Santiago M. Mola 1a6df12902 fix Coq sample JsNumber.v (#3710)
It was fetched as HTML from GitHub instead of raw.
2017-07-10 09:41:36 +01:00
Alhadis 4f1e5c34b1 Add permissive-licensed Coq samples
BSD-2-Clause: https://github.com/jscert/jscert

  * JSCorrectness.v
  * JSInterpreterExtraction.v
  * JSNumber.v
  * JSPrettyInterm.v

MIT/Expat: https://github.com/clarus/coq-atm

  * Computation.v
  * Main.v
  * Spec.v
2016-11-03 02:50:54 +11:00
Alhadis 85c9833081 Delete GPL2.1-licensed Coq samples
These files are modified variants of the ones included in Coq's standard
distribution. The original materials feature the GPL 2.1 license in each
file's header, which was suspiciously removed from Linguist's samples.

    https://github.com/coq/coq/tree/trunk/theories

Basics.v is a different file to that found in Coq's distro, but is vague
in origin and being removed to err on the side of caution. The remaining
samples are from a MIT-licensed online course by Software Foundations:

    https://www.cis.upenn.edu/~bcpierce/sf/current/

References: github/linguist#3313
2016-11-03 02:32:23 +11:00
Joshua Peek 2b36f73da6 Some comments are triggering charlock binary 2012-09-24 10:48:22 -05:00
Joshua Peek 7b6caa0f6c Rename samples subdirectories 2012-07-23 15:52:49 -05:00