diff options
| author | Hugo Herbelin | 2016-06-01 20:52:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-02 14:16:11 +0200 |
| commit | 39741ee5b9c5ea1948e2a97e00e362eea6d936d0 (patch) | |
| tree | a53a512eb36f066804382c4d7943f2daf770f910 /dev | |
| parent | 5cb0d0590eb01e0122c37904dbfdd53f0405d7f4 (diff) | |
Removing pointless field NPatVar. It does not make sense to have Meta
and Evar in notations, and there are anyway already forbidden.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions