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 /plugins/ltac | |
| 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 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 5a26ac8827..bec83411c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -62,7 +62,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = - Pcoq.Entry.of_parser "lpar_id_colon" + Pcoq.G.Entry.of_parser "lpar_id_colon" (fun _ strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with |