blob: a20ad1b4dab22dc5aec7c4d9fa67c5e2a8952e81 (
plain)
1
2
3
4
5
|
(* Slightly improving interpretation of Ltac subterms in notations *)
Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e)
..)) (at level 200, x binder, y binder, e at level 220).
Check (var2 a = 1; a).
|
