diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-07 16:19:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 20:44:29 +0200 |
| commit | e1e750683d52e7d2b63a707b62c4d2af0e01a532 (patch) | |
| tree | 4784d8750155dee00501bfa80765b2a7f8ffc8c0 /dev/doc | |
| parent | 6522aa62d832837314dcef54735e6a4e55431571 (diff) | |
Isolating a function "make_abstraction", new name of "letin_abstract",
which compute an abstraction of the goal over a term or a pattern.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8a2b13ebe..d4e42142b 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -75,7 +75,8 @@ check_evars_are_solved explicitly to check that evars are solved. See also the corresponding commit log. -- Tactics API: new_induct -> induction; new_destruct -> destruct +- Tactics API: new_induct -> induction; new_destruct -> destruct; + letin_pat_tac do not accept a type anymore ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = |