The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 10/12/2016 05:03 PM, Clément Pit--Claudel wrote:
> Hi coq-club,
>
> The CHANGES file says:
>
>      - Matching using "lazymatch" was fundamentally modified. It now behaves
>        like "match" (immediate execution of the matching branch) but without
>        the backtracking mechanism in case of failure.
>
> The description of the new behaviour sounds close to what my understanding of 
> lazymatch was in 8.4 (as long as the result of the lazy match isn't bound to 
> a variable).  Beyond the 8.4 issue that caused lazymatch to backtrack when a 
> branch contained a type error, what are examples of differences between the 
> old and the new lazymatch?
>
> Thanks!
> Clément.

Unfortunately, I don't have an 8.4 around to test this on - but AFAIR 
lazymatch prior to 8.5 didn't have the greedy evaluation of branches 
behavior as does (and did) match.  Hence, something like:

Goal True.
let x := lazymatch goal with _ => idtac "hello" end in
idtac "there".

in 8.4 would just print "there" and not "hello" "there".

-- Jonathan