diff options
| author | Arnaud Spiwack | 2014-11-14 09:40:23 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-19 10:11:45 +0100 |
| commit | bd2dd62ea83ff9374bd28f089b19d3abba6ac7cb (patch) | |
| tree | 9be4b23ec2ae2f6d83c1d1d45eedf0bfe74611d3 /kernel | |
| parent | 9e1224f452470c3e18e13c88c4d8a00fe0864c16 (diff) | |
Glob-ops: a name-mapping operation for pattern-matching binders.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions