From d3169b50e5ff8a2942829f86dc6482fe5ddfac1b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Mon, 18 Dec 2017 11:54:05 +0100
Subject: [PATCH] Start working on a CHANGELOG.
---
CHANGELOG.md | 47 +++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 47 insertions(+)
create mode 100644 CHANGELOG.md
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..3d52be9
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,47 @@
+This file lists "large-ish" changes to the std++ Coq development, but not every
+API-breaking change is listed.
+
+## std++ 1.1.0 (unfinished)
+
+New features:
+
+- Many new lemmas about lists, vectors, sets, maps.
+- Equivalence proofs between coq++ functions that have a different definition in
+ the Coq standard library, e.g. `List.nth`, `List.NoDop`.
+- Type versions of the logical connectives and list predicates:
+ `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
+- A connective `tc_opaque` to make definitions type class opaque.
+- A type class `Infinite` for infinite types.
+- A generic implementation to obtain fresh elements of infinite types.
+- More theory about curry and uncurry functions on `gmap`.
+- A generic `filter` and `zip_with` operation on finite maps.
+- A type of generic trees for showing that arbitrary types are countable.
+
+Changes:
+
+- Get rid of `Automatic Coercions Import`, it is deprecated.
+- `Hint Mode` is now set for all operational type classes to make instance
+ search less likely to diverge.
+- New type class `RelDecision` for decidable relations, and `EqDecision` is
+ defined in terms of it. This class allows to set `Hint Mode` properly.
+- Use the flag `assert` of `Arguments` to make it more robust.
+- The functions `imap` and `imap2` on lists are defined so that they enjoy more
+ definitional equalities.
+- Theory about `fin` is moved to its own file `fin.v`.
+- Rename `preserving` → `mono`.
+
+Changes to notations:
+
+- Operational type classes for lattice notations: `⊑`,`⊓`, `⊔`, `⊤` `⊥`.
+- Replace `⊥` for disjointness with `##`, so that `⊥` can be used for the
+ bottom lattice element.
+- All notations are now in `stdpp_scope` with scope `stdpp`
+ (formerly `C_scope` and `C`).
+- Stronger binding for `.1` and `.2` that is compatible with ssreflect.
+- Various changes to monadic notation to improve compatibility with Mtac2:
+ + Pattern matching notation for monadic bind `'pat ← x; y` where `pat` can
+ be any Coq pattern.
+ + Change the level of the do-notation.
+ + `<$>` is left associative.
+ + Notation `x ;; y` for `_ ← x; y`.
+-
--
2.26.2