blob: b8c93679519bb57d8803c0475b595683335a326f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Check that uconstrs are interpreted in the ltac-substituted environment *)
(* Was a regression introduced in 4dab4fc (#7288) *)
Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) :=
set (h := fun x => f).
Fact test : nat -> nat.
Proof.
intros n.
bind n in (n*n) as f.
assert (f 0 = 0) by reflexivity.
Abort.
|
