[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.

1 files changed, 3 insertions, 4 deletions

diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index fb91ea7b5c..9d75341795 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -98,18 +98,17 @@ let tokenize_string s =
     else
       stream_tok ((Tok.extract_string true e) :: acc) str
   in
-  let st = CLexer.get_lexer_state () in
+  let st = CLexer.Lexer.State.get () in
   try
     let istr = Stream.of_string s in
     let lex = CLexer.LexerDiff.tok_func istr in
     let toks = stream_tok [] (fst lex) in
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     toks
   with exn ->
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     raise (Diff_Failure "Input string is not lexable");;
 
-
 type hyp_info = {
   idents: string list;
   rhs_pp: Pp.t;