diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-27 15:05:36 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-10 23:50:22 +0200 |
commit | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (patch) | |
tree | 6bde0d640de16eec21b6e93b73ffac1a96e18b6c /test-suite/output | |
parent | b6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (diff) |
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"
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/SuggestProofUsing.out | 7 | ||||
-rw-r--r-- | test-suite/output/SuggestProofUsing.v | 31 |
2 files changed, 38 insertions, 0 deletions
diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out new file mode 100644 index 000000000..97cb0fdd8 --- /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 000000000..b0b514a52 --- /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. |