diff options
| author | Emilio Jesus Gallego Arias | 2019-02-05 17:22:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-05 17:22:35 +0100 |
| commit | d23434f0c05e185842667daf7ffbcb8410db41c0 (patch) | |
| tree | 510b299016e34a0e31cf2289757f86c5e041cd6e /kernel/nativecode.ml | |
| parent | d9afe70c9c65359b6eb827f5b30d84f24074efa1 (diff) | |
[parsing] Use AST node for main parsing entry.
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions