diff options
| author | Pierre Courtieu | 2020-04-10 13:08:29 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-10 13:08:29 +0200 |
| commit | d1053a06aa31ce05fa0741fb61dfb1266fcb0364 (patch) | |
| tree | 67c8ef6766a8b890f5e5656462fd1afe654af1ae /pgshell/example.pgsh | |
| parent | 4dba3f78e50604d899ef80bfda45c5aa4467adeb (diff) | |
Fixed proof using annotation mechanism.
I ended up using (in a slight devious way) the lemma dependency
mechanism of PG: the dependency information stored in the span is only
the ones suggested by coq: only the one that should appear in theproof
using annotation (and only when coq felt the need to suggest them.
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions