diff options
| author | Pierre-Marie Pédrot | 2019-02-05 17:10:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-11 15:48:43 +0100 |
| commit | ccfa2585dbe9a482040f2b2d405fdb4451d19e39 (patch) | |
| tree | 80f24ac2a46c77bde95196c09551378322e24922 /kernel/type_errors.ml | |
| parent | 9352347ee0ea77e0095145afe8c4824a4d5ca32c (diff) | |
Move most of Gramext into Grammar.
This module was defining unsafe functions and datatypes only relevant to the
grammar engine. We hide them under the API so as to be able to later clean
it up.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions