diff options
| author | Pierre-Marie Pédrot | 2016-04-24 16:57:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-24 19:16:33 +0200 |
| commit | ea984528e269fa34afa3dd1757a00ff5a8405157 (patch) | |
| tree | ba5ac9ac92644b976d97809709e8962806920a32 /plugins/syntax | |
| parent | b090942f20ac8854bf227698d31ca1efec492c47 (diff) | |
Disentangle tactic notation resolution from Pcoq.
Instead of relying on entry names as given by a hardwired registering
scheme in Pcoq, we recover them first through a user-defined map, and
fallback on generic argument names.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions