blob: bcb73f8fd069ba5ce2b664da00cfa222c04eec3b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
Unreleased changes
==================
<!-- Until https://github.com/coq/coq/pull/9964 is merged, we continue
adding changelog entry here. -->
**Kernel**
**Specification language, type inference**
**Notations**
**Tactics**
**Tactic language**
- Modes are now taken into account by `typeclasses eauto` for local hypotheses.
**SSReflect**
- `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
- New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
class, simplified `predType` interface: `pred_class` and `mkPredType`
deprecated, `{pred T}` and `PredType` should be used instead.
- `if c return t then ...` now expects `c` to be a variable bound in `t`.
- New `nonPropType` interface matching types that do _not_ have sort `Prop`.
- New `relpre R f` definition for the preimage of a relation R under f.
**Commands and options**
**Tools**
**CoqIDE**
**Standard library**
- Added Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull
**Infrastructure and dependencies**
**Miscellaneous**
Released changes
================
See <https://coq.github.io/doc/master/refman/changes.html>.
|
