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 /user-contrib | |
| 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 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 0946c88228..920be6db5b 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1590,7 +1590,7 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu) type seqrule = -| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule +| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule let rec make_seq_rule = function | [] -> |