diff options
| author | Vincent Laporte | 2018-12-06 09:07:24 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-12-06 09:07:24 +0000 |
| commit | a2c8b7df8a0702ab716c0b97ad63d235b58b93a0 (patch) | |
| tree | c3320b64340018f5a73d111c3fefc79b4c507741 /pretyping/patternops.ml | |
| parent | 5331889da2d3f57f7aed935f6456e39765eb8b31 (diff) | |
| parent | 90ae85437a281ca655f7e9511ef09874ba591857 (diff) | |
Merge PR #8917: Small cleanup wrt attributes_of_flags and template attribute
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions