diff options
| author | Emilio Jesus Gallego Arias | 2017-07-31 14:06:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-07-31 14:06:02 +0200 |
| commit | 1c55826018c5f07ee25b5771e59fe0389293cb62 (patch) | |
| tree | 7e9f641d39a29e5848c4e8bc90b9702dc793c899 /kernel/nativelib.ml | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
[general] Remove spurious dependency of highparsing on toplevel.
`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.
This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions