diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-31 14:18:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-29 17:21:57 +0200 |
| commit | 73d577c2d959de975415f2807df6a22fa392d335 (patch) | |
| tree | 152922be2f8f646cf2b5ce9ce5fe7979cb60bafe /intf/constrexpr.ml | |
| parent | f1806ab001cfbc9548e607397fc55b9c1be7c25b (diff) | |
[parsing] Remove hacks for reduced Prelude.
These hacks to warn the users about needed modules are not needed
anymore in 8.8, as the proper error message is done in 8.7 already.
This helps in avoiding a dependency from parsing to MlTop.
Diffstat (limited to 'intf/constrexpr.ml')
0 files changed, 0 insertions, 0 deletions