diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 03:22:22 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:55:41 +0200 |
| commit | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (patch) | |
| tree | 24b4e369c4acbe2bb9c9ca79b84fc7ddff34e2d8 /plugins/ssrmatching | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
[camlpX] Remove camlp4 compat layer.
We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.
We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 4d5594633..3d0232d94 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -10,7 +10,7 @@ (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.freeze () ;; +let frozen_lexer = CLexer.get_keyword_state () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) @@ -1040,7 +1040,7 @@ let interp_open_constr ist gl gc = let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c let interp_term ist gl (_, c) = (interp_open_constr ist gl c) let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with +let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' @@ -1057,8 +1057,6 @@ ARGUMENT EXTEND cpattern | [ "Qed" constr(c) ] -> [ mk_lterm c ] END -let (!@) = Compat.to_coqloc - GEXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> @@ -1444,6 +1442,6 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = CLexer.unfreeze frozen_lexer ;; +let () = CLexer.set_keyword_state frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) |