From 10e90e268d874b58bf4462677d20dcb893ed0588 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 8 Jun 2020 09:18:34 +0200
Subject: Don't suggest Proof using when no section variables

Fix #12447
---
 test-suite/output/SuggestProofUsing.out | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'test-suite/output/SuggestProofUsing.out')

diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
index 8d67a4a4b7..010e217efb 100644
--- a/test-suite/output/SuggestProofUsing.out
+++ b/test-suite/output/SuggestProofUsing.out
@@ -1,7 +1,11 @@
-The proof of nat should start with one of the following commands:
+The proof of Nat should start with one of the following commands:
 Proof using . 
 Proof using Type*. 
 Proof using Type. 
 The proof of foo should start with one of the following commands:
 Proof using A B. 
 Proof using All. 
+The proof of sec_exactproof should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
-- 
cgit v1.2.3