diff options
| author | Pierre-Marie Pédrot | 2018-06-22 12:24:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-07 16:34:44 +0200 |
| commit | ef29c0a927728d9cf4a45bc3c26d2393d753184e (patch) | |
| tree | d43b108a24ac69f7fbcdd184781141fea36a1dd5 /toplevel/coqloop.mli | |
| parent | 4b3187a635864f8faa2d512775231a4e6d204c51 (diff) | |
Introduce a Pcoq.Entry module for functions that ought to be exported.
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
Diffstat (limited to 'toplevel/coqloop.mli')
| -rw-r--r-- | toplevel/coqloop.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 5c07a8bf3b..b11f13d3cb 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -18,7 +18,7 @@ type input_buffer = { mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) (** The input buffer of stdin. *) |