aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/proof_using.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-27 15:05:36 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-10-10 23:50:22 +0200
commitffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (patch)
tree6bde0d640de16eec21b6e93b73ffac1a96e18b6c /vernac/proof_using.ml
parentb6d4575e39d32d276bed84ccb6b2b67a2e7bccb6 (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 'vernac/proof_using.ml')
0 files changed, 0 insertions, 0 deletions