diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 12:20:00 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | af7628468d638c77fb3f55a9eb315b687b76a21d (patch) | |
| tree | 63cfb1a71815b956d5a79cf83b4d5284626d1d1e /vernac/pvernac.ml | |
| parent | f9174f64c56375adb42e53b97df9eeb8b0a9680d (diff) | |
[parsing] Remove redundant interfaces from Pcoq
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
Diffstat (limited to 'vernac/pvernac.ml')
| -rw-r--r-- | vernac/pvernac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 9a9c96064d..26364ed075 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -65,8 +65,8 @@ module Vernac_ = | Some ename -> find_proof_mode ename let command_entry = - Pcoq.Entry.of_parser "command_entry" - (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) + Pcoq.G.Entry.of_parser "command_entry" + (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) end |