diff options
| author | Hugo Herbelin | 2020-04-15 15:55:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-05 19:09:07 +0100 |
| commit | c893dc56fa579c8d1f6ea3a1859681bb316d9979 (patch) | |
| tree | 1985fd6284f70466b5640d38c97bef3465ceddc3 /interp/constrintern.ml | |
| parent | 4b8a87bcebe23797c4a179dd6a1d55c058d2736f (diff) | |
Accept section variables in notations with mixed terms and binders.
Diffstat (limited to 'interp/constrintern.ml')
0 files changed, 0 insertions, 0 deletions