From 607d8b9f76d3cae81003b98dacc80bc9cf9967a2 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sat, 30 May 2020 12:04:18 +0200 Subject: [PATCH 1/2] Create README.md --- reals/faster/README.md | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 reals/faster/README.md diff --git a/reals/faster/README.md b/reals/faster/README.md new file mode 100644 index 00000000..7cfd43ad --- /dev/null +++ b/reals/faster/README.md @@ -0,0 +1,9 @@ +The files in this directory correspond to the formalization in: + +Robbert Krebbers and Bas Spitters, _Type classes for efficient exact real arithmetic in Coq_ +LMCS 9(1:1), 2013. 10.2168/LMCS-9(1:01)2013. [arXiv 1106.3448](http://arxiv.org/abs/1106.3448/) + +The code may be used under the following licenses: +* GPL 2.0 and later +* LGPL 2.1 and later +* WTFPL From 110c8459882fdeb4516dd304704e30ba97f1dfb6 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Thu, 6 Aug 2020 13:23:53 +0200 Subject: [PATCH 2/2] Update README.md --- reals/faster/README.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/reals/faster/README.md b/reals/faster/README.md index 7cfd43ad..68f864f7 100644 --- a/reals/faster/README.md +++ b/reals/faster/README.md @@ -1,9 +1,6 @@ -The files in this directory correspond to the formalization in: +The files in this directory correspond to the formalization presented in: Robbert Krebbers and Bas Spitters, _Type classes for efficient exact real arithmetic in Coq_ LMCS 9(1:1), 2013. 10.2168/LMCS-9(1:01)2013. [arXiv 1106.3448](http://arxiv.org/abs/1106.3448/) -The code may be used under the following licenses: -* GPL 2.0 and later -* LGPL 2.1 and later -* WTFPL +The code is available under the MIT license.