From ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 15:05:36 +0200
Subject: Take Suggest Proof Using outside the kernel.

Also add an output test for Suggest Proof Using.

This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"

For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"
---
 test-suite/output/SuggestProofUsing.out |  7 +++++++
 test-suite/output/SuggestProofUsing.v   | 31 +++++++++++++++++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 test-suite/output/SuggestProofUsing.out
 create mode 100644 test-suite/output/SuggestProofUsing.v

(limited to 'test-suite')

diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
new file mode 100644
index 0000000000..97cb0fdd89
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.out
@@ -0,0 +1,7 @@
+The proof of Top#Sec#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. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
new file mode 100644
index 0000000000..b0b514a52b
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.v
@@ -0,0 +1,31 @@
+Set Suggest Proof Using.
+
+Section Sec.
+  Variables A B : Type.
+
+  (* Some normal lemma. Sadly the internal name gets printed. *)
+  Lemma nat : Set.
+  Proof.
+    exact nat.
+  Qed.
+
+  (* Make sure All is suggested even though we add an unused variable
+  to the context. *)
+  Let foo : Type.
+  Proof.
+    exact (A -> B).
+  Qed.
+
+  (* Having a [Proof using] disables the suggestion message. *)
+  Definition bar : Type.
+  Proof using A.
+    exact A.
+  Qed.
+
+  (* Transparent definitions don't get a suggestion message. *)
+  Definition baz : Type.
+  Proof.
+    exact A.
+  Defined.
+
+End Sec.
-- 
cgit v1.2.3


From a627891e0505e7da7afcb56c79d2058ebf058694 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 16:45:29 +0200
Subject: Use a nice printer for constant names in Suggest Proof Using.

---
 test-suite/output/SuggestProofUsing.out | 2 +-
 test-suite/output/SuggestProofUsing.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
index 97cb0fdd89..8d67a4a4b7 100644
--- a/test-suite/output/SuggestProofUsing.out
+++ b/test-suite/output/SuggestProofUsing.out
@@ -1,4 +1,4 @@
-The proof of Top#Sec#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. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
index b0b514a52b..00b6f8e183 100644
--- a/test-suite/output/SuggestProofUsing.v
+++ b/test-suite/output/SuggestProofUsing.v
@@ -3,7 +3,7 @@ Set Suggest Proof Using.
 Section Sec.
   Variables A B : Type.
 
-  (* Some normal lemma. Sadly the internal name gets printed. *)
+  (* Some normal lemma. *)
   Lemma nat : Set.
   Proof.
     exact nat.
-- 
cgit v1.2.3