diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-22 11:06:04 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-07 16:34:43 +0200 |
commit | 4b3187a635864f8faa2d512775231a4e6d204c51 (patch) | |
tree | 6ed32cd7b3f8530336c43137f0603200dc69098b /vernac | |
parent | fe371675fc85d712f5124d73157bd833e8fa14a6 (diff) |
Remove dead code that used to be there for CamlpX compatibility.
Part of this code has been introduced very recently in 7c62654 in spite of
the existence of a proper API. This means that this should be better
documented.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/pvernac.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index bac882381..aea66a07a 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -10,8 +10,6 @@ open Pcoq -let uncurry f (x,y) = f x y - let uvernac = create_universe "vernac" module Vernac_ = @@ -32,18 +30,19 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in + let open Extend in + let act_vernac v loc = Some (loc, v) in + let act_eoi _ loc = None in let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); + Rule (Next (Stop, Atoken Tok.EOI), act_eoi); + Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in - uncurry (Gram.extend main_entry) (None, [None, None, rule]) + Pcoq.grammar_extend main_entry None (None, [None, None, rule]) let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) end |