blob: 841f77febbae5689151bab5c9f80dc0d8d456302 (
plain)
1
2
3
4
5
6
7
8
9
|
Ltac bar x := pose x.
Tactic Notation "foo" open_constr(x) := bar x.
Class baz := { baz' : Type }.
Goal True.
(* Original error was an anomaly which is fixed; now, it succeeds but
leaving an evar, while calling pose would not leave an evar, so I
guess it is still a bug in the sense that the semantics of pose is
not preserved *)
foo baz'.
|
