From 320363315e350bf427054d837a02b4d97f015199 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 22 Dec 2018 01:45:30 +0100
Subject: Fix #9272: `Unset Nested Proofs Allowed` does not capture nested
 `Instance` proofs.

We forbid commands that may open proofs inside proofs.
---
 test-suite/bugs/opened/bug_3890.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 5c74addb62..78b2aa69b9 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -1,3 +1,5 @@
+Set Nested Proofs Allowed.
+
 Class Foo.
 Class Bar := b : Type.
 
-- 
cgit v1.2.3