diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 12:46:22 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:01 -0400 |
| commit | f374c2562b9522bd90330f6f17f0a7e41c723e8b (patch) | |
| tree | 3ad126603fb6a7eccb1ec20b3dc3dd340cf22b90 /parsing/pcoq.mli | |
| parent | af7628468d638c77fb3f55a9eb315b687b76a21d (diff) | |
[parsing] Move `coq_parsable` custom logic to Grammar.
Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.
The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.
This PR doesn't solve that but it is a step towards a more functional
solution.
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0352c1d55b..5d21b39dee 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,14 +15,9 @@ open Libnames (** The parser of Coq *) -module G : sig - - include Gramlib.Grammar.S - - val comment_state : Parsable.t -> ((int * int) * string) list - -end with type te = Tok.t and type 'a pattern = 'a Tok.p +module G : Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p +(** Compatibility module, please avoid *) module Entry : sig type 'a t = 'a G.Entry.t val create : string -> 'a t |