diff options
| author | Hugo Herbelin | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /dev/doc | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index cea4cf1224..d872110b97 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -91,8 +91,11 @@ "intros_pattern" and "intros_patterns" is not anymore behaving like tactic "intros" on the empty list. -- API of cut tactics changed: cut_intro should be replaced by - "enough_tac Anonymous" +- API of cut tactics changed: for instance, cut_intro should be replaced by + "assert_after Anonymous" + +- All functions taking an env and a sigma (or an evdref) now takes the + env first. ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = |