diff options
| author | Pierre Courtieu | 2020-04-09 15:20:09 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-09 15:20:09 +0200 |
| commit | d3ac65007d676d57569d764b493d4d8d6f6ed1cb (patch) | |
| tree | 7b821dfe990af0d7e9734b921bad189b8705f4b3 /pgshell/example.pgsh | |
| parent | 9196749d55413224355409d55003f7f8c8ba0f79 (diff) | |
Automatic "Proof using" insertion.
When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions