diff options
| author | Pierre Courtieu | 2013-07-10 11:45:10 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-07-10 11:45:10 +0000 |
| commit | c3cf9716040b613afecab125a3de97f6a7052f05 (patch) | |
| tree | 865b00112675e03cc6fa701471b141193c09f27c /pgshell | |
| parent | a169507920a0116839a32b691d095be7106932c7 (diff) | |
Fixing #475. the "=>" ptoken just before "exists" should be the ltac
"=>" most of the time.
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions