diff options
| author | Pierre-Marie Pédrot | 2020-03-31 00:48:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 00:48:42 +0200 |
| commit | e2f0814688511be93659c2258b91248698f18d4a (patch) | |
| tree | 06c1860a6e5b45ee154e45bfbddfff228ac22cdd /printing | |
| parent | 8c85a8651605dd82ce2223a28ca38f31359a88bd (diff) | |
| parent | 5c9f318f5f1b6e85b03bba9450ac059377be54fc (diff) | |
Merge PR #11647: [rfc] Consolidation of parsing interfaces
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/proof_diffs.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index d73d1f2d1a..3a6424ba9f 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -96,18 +96,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; |
