diff options
| author | Pierre-Marie Pédrot | 2018-11-24 17:49:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-05 17:57:46 +0100 |
| commit | c03c4ea72e920bf69f29b9ef48c7be64c504d293 (patch) | |
| tree | 50a3135f8988c49a48645718301f8e7619048bf4 /dev/base_include | |
| parent | d85a200cb8fca964bb7428ca6a607cfc9dc83c79 (diff) | |
Remove the grammar-entry correspondence dynamic check in camlp5.
Due to the fact we only export the functorial API, this property is ensured
statically. There is thus no point in checking it.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions