aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/sideff.v
blob: 3c0b81568afbaffffa2df1da547769bd09d8cb11 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Definition idw (A : Type) := A.
Lemma foobar : unit.
Proof.
  Require Import Program.
  apply (const tt tt).
Qed.

Lemma foobar' : unit.
  Lemma aux : forall A : Type, A -> unit.
  Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
  apply (@aux unit tt).
Qed.