The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

According to https://coq.inria.fr/distrib/V8.5/CHANGES:

- Tactic "refine" has been changed back to the 8.4 behavior of shelving 
subgoals
  that occur in other subgoals. The "refine" tactic of 8.5beta3 has been
  renamed "simple refine"; it does not shelve any subgoal.

However, in my experience, refine still behaves differently in Coq 8.5
than it did in 8.4.  For example:

Goal forall f : nat -> nat,
  (forall m n:nat, m <= n -> f m <= f n) ->
  f 1 <= 5 -> f 0 <= 5.
Proof.
intros f fincr f1.
refine (let H := fincr 0 1 _ in _).

In 8.4, this would produce two subgoals (Γ |- 0 <= 1; Γ, H : f 0 <= f
1 |- f 0 <= 5).  However, in 8.5 it produces a single goal (Γ, H :=
fincr 0 1 ?existential |- f 0 <= 5).  It seems to get the 8.4 behavior
back, I need "simple refine (let H := fincr 0 1 _ in _); [|clearbody
H]", or the same with unshelve refine.

So, am I completely misunderstanding that CHANGES entry, or is it
inaccurate?  (I'm using the Debian 8.5-2 packages.)
–
Daniel Schepler