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

Set Nested Proofs Allowed.

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.