diff options
| author | Gaëtan Gilbert | 2019-04-11 12:45:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-30 22:48:25 +0200 |
| commit | 77257819ea4a381067e65fd46e7d7590aa7e2600 (patch) | |
| tree | efba4f3a1a68ca658a350e3bb310fed1a69bb488 /interp/implicit_quantifiers.ml | |
| parent | bb4f304848e04c492d98db5da0bdb1895cecc191 (diff) | |
Remove Global.env from goptions by passing from vernacentries
Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions