Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
coqstdpp
Commits
d3169b50
Commit
d3169b50
authored
Dec 18, 2017
by
Robbert Krebbers
Browse files
Start working on a CHANGELOG.
parent
20fb85af
Changes
1
Hide whitespace changes
Inline
Sidebyside
CHANGELOG.md
0 → 100644
View file @
d3169b50
This file lists "largeish" changes to the std++ Coq development, but not every
APIbreaking 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 donotation.
+
`<$>`
is left associative.
+
Notation
`x ;; y`
for
`_ ← x; y`
.

Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment