The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/25/2014 12:31 PM, Jonathan wrote:
> On 07/25/2014 12:11 PM, Jason Gross wrote:
> > This is untested, but I think the following should work:
> >
> > lazymatch goal with
> >    | [ |- ?lhs = ?e ?x ] => let lhs' := (eval pattern x in lhs) in 
> > change
> > (lhs' = e x)
> > end
>
> That works!  Thanks.  I didn't know that pattern was one of the 
> tactics accepted by compute.  But - now I see it in the refman (page 
> 249-250).
>
> By the way, reflexivity doesn't work on the result, but unify does via:
>
> match goal with |- ?A = ?B => unify A B end.
>
> Shouldn't reflexivity be doing that?  Auto works as well, but since 
> info_auto doesn't work, I don't know what auto did.

Oh - I forgot about debug.  Using debug auto, it says that auto 
succeeded via apply @eq_refl, which is surprising since I though 
reflexivity did the same thing.

-- Jonathan