diff options
Diffstat (limited to 'test-suite/success/sideff.v')
| -rw-r--r-- | test-suite/success/sideff.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v index 3c0b8156..b9a1273b 100644 --- a/test-suite/success/sideff.v +++ b/test-suite/success/sideff.v @@ -5,6 +5,8 @@ Proof. 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. |