diff options
| author | Pierre-Marie Pédrot | 2016-02-24 10:26:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-24 10:31:17 +0100 |
| commit | d96bf1b1ec79fa93787d23e1c42f803d74b49321 (patch) | |
| tree | 96f23cdf57def01387e8ad7155ba5305bb3ec132 /kernel | |
| parent | ee162ba3b28fccca0a2b3ea4b1e0811006840570 (diff) | |
Removing the METAIDENT token, as it is not used anymore.
METAIDENT were idents of the form $foobar, only used in quotations.
Note that it removes two dollars in the Coq codebase! Guess I'm absolved
for the $(...) syntax.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions