Does ltac `match`

/`lazymatch`

not work for open terms (`constr_under_binder`

)?

```
Ltac f M :=
match M with
| (fun x => ?M) => f M
| _ => idtac M
end.
Goal False. let M := f (fun x => x) in idtac M.
(* Error:
Must evaluate to a closed term
offending expression:
M
this is an object of type constr_under_binders
*)
```

Last updated: Jun 22 2024 at 16:02 UTC