From 42853370f42163fff4b4743b98a1298daaf140b1 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 6 Nov 2017 17:24:15 +0100
Subject: [PATCH] Version 0.88.1

---
 .gitattributes     | 22 +++++++++++++---------
 CHANGES.md         |  9 +++++++--
 README.md          |  4 ++--
 Version            |  2 +-
 doc/manual.tex     |  2 +-
 opam/why3-base/url |  2 --
 opam/why3/opam     |  2 +-
 7 files changed, 25 insertions(+), 18 deletions(-)
 delete mode 100644 opam/why3-base/url

diff --git a/.gitattributes b/.gitattributes
index 5084fc5bf..e90c3102c 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,12 +1,16 @@
-/examples/in_progress/ export-ignore
-/examples/hoare_logic/draft/ export-ignore
-/tests/ export-ignore
-/bench/encoding/ export-ignore
-/misc/ export-ignore
-/ROADMAP export-ignore
-/DEVELOPER.readme export-ignore
-/opam/ export-ignore
-.gitignore export-ignore
 .gitattributes export-ignore
+.gitignore export-ignore
+.keepme export-ignore
+
+/.gitlab-ci.yml export-ignore
+/.mailmap export-ignore
 /check.sh export-ignore
+/DEVELOPER.readme export-ignore
+/ROADMAP export-ignore
 /TODO export-ignore
+
+/bench/encoding/ export-ignore
+/examples/in_progress/ export-ignore
+/misc/ export-ignore
+/opam/ export-ignore
+/tests/ export-ignore
diff --git a/CHANGES.md b/CHANGES.md
index c8f1998da..a4e52a8b2 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,13 +1,18 @@
 :x: marks a potential source of incompatibility
 
-Version 0.88.1, ?, 2017
+Version 0.88.1, November 6, 2017
 -----------------------
 
 API
-  * export function `Call_provers.get_new_results`
+  * exported function `Call_provers.get_new_results`
 
 Provers
   * improved support for Isabelle 2017
+  * fixed support for Coq 8.7
+
+Miscellaneous
+  * fixed compilation for OCaml 4.06
+  * improved support for nullary `val` declarations with regions
 
 Version 0.88.0, October 6, 2017
 -------------------------------
diff --git a/README.md b/README.md
index a0706d641..d9bbd5979 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,5 @@
-WHY 3
-=====
+WHY3
+====
 
 Why3 is a platform for deductive program verification. It provides
 a rich language for specification and programming, called WhyML, and
diff --git a/Version b/Version
index 4fe551ddc..5cab4a37b 100644
--- a/Version
+++ b/Version
@@ -1,2 +1,2 @@
 # Why version
-VERSION=0.88.0
+VERSION=0.88.1
diff --git a/doc/manual.tex b/doc/manual.tex
index 2fae9c298..ef95d4000 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -108,7 +108,7 @@
 %BEGIN LATEX
 \begin{LARGE}
 %END LATEX
-  Version \whyversion{}, October 2017
+  Version \whyversion{}, November 2017
 %BEGIN LATEX
 \end{LARGE}
 %END LATEX
diff --git a/opam/why3-base/url b/opam/why3-base/url
deleted file mode 100644
index e2f15064d..000000000
--- a/opam/why3-base/url
+++ /dev/null
@@ -1,2 +0,0 @@
-archive: "https://gforge.inria.fr/frs/download.php/file/37147/why3-0.88.0.tar.gz"
-checksum: "1aef885ff8eee34107585e11db623a8d"
diff --git a/opam/why3/opam b/opam/why3/opam
index 9bbb253fc..86b773b72 100644
--- a/opam/why3/opam
+++ b/opam/why3/opam
@@ -23,7 +23,7 @@ tags: [
 ]
 available: [ ocaml-version >= "4.02.3" ]
 depends: [
-  "why3-base" { = "0.88.0" }
+  "why3-base" { = "0.88.1" }
   "lablgtk"
   "conf-gtksourceview"
   "zarith"
-- 
GitLab