blob: 5f1785c706523ab85aaf09a8d41b3696f5847f0f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Tactic Notation "opose" open_constr(foo) := pose foo.
Class Foo := Build_Foo : Set.
Axiom f : forall `{Foo}, Set.
Set Printing Implicit.
Goal forall `{Foo}, True.
Proof.
intro H.
pose f.
opose f.
Fail let x := (eval hnf in P) in has_evar x.
let x := (eval hnf in P0) in has_evar x.
|
