diff options
| author | Hugo Herbelin | 2020-11-03 02:11:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 17:33:43 +0100 |
| commit | 091bfff6ce37a303550e79abb23fdc992a28f7e3 (patch) | |
| tree | 1c58695f2aa1d658fde2ff09a90c267cb0e2dc9a /interp/notation.ml | |
| parent | 7f90e6e0aa8dd27c64bac0dbc4b247ebb33d4aca (diff) | |
Fixes #13298: primitive projections needs a correct typing environment.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions