diff options
| author | Hugo Herbelin | 2017-08-15 01:11:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:05 +0100 |
| commit | 6480c7e1d89558252f2e8a8f1b7d3b03f7ef6a74 (patch) | |
| tree | eafb752070dac9baf8b80903ef9243ca505a5dd0 /interp/notation_ops.ml | |
| parent | 96d6ef7036e19bf1def1512abae5ef8c6ace06b0 (diff) | |
Make pattern variables of "match" substitutable in notations.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions