diff options
| author | Hugo Herbelin | 2015-07-30 19:20:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 15:06:53 +0200 |
| commit | cb0dea2a0c2993d4ca7747afc61fecdbb1c525b1 (patch) | |
| tree | e910d8dd975bf7a2716ae94fe457409f0d0b2da1 | |
| parent | 1eb48ca8695a26fa5ca248a2201a164f90885360 (diff) | |
Documenting change of behavior of apply when the lemma is a tuple and
applying a component of the tuple.
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 4 insertions, 1 deletions
@@ -35,7 +35,6 @@ API * A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated. - Tools - Added an option -w to control the output of coqtop warnings. @@ -359,6 +358,10 @@ Tactics trace anymore. Use "Info 1 auto" instead. The same goes for "info_trivial". On the other hand "info_eauto" still works fine, while "Info 1 eauto" prints a trivial trace. +- When using a lemma of the prototypical form "forall A, {a:A & P a}", + "apply" and "apply in" do not instantiate anymore "A" with the + current goal and use "a" as the proof, as they were sometimes doing, + now considering that it is a too powerful decision. Program |