diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 02:35:56 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 (patch) | |
| tree | a4204cd4bced576d6d846ebac908aab5092c66a5 /vernac/pvernac.ml | |
| parent | 4a88beff476d2c27eae381bc8a61f777015c0617 (diff) | |
[parsing] Make grammar extension type private.
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
Diffstat (limited to 'vernac/pvernac.ml')
| -rw-r--r-- | vernac/pvernac.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 08625b41a6..aebded72f8 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -51,12 +51,11 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let open Extend in let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ - Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); - Rule (Next (Stop, Aentry vernac_control), act_vernac); + Rule (Next (Stop, Pcoq.G.Symbol.token Tok.PEOI), act_eoi); + Rule (Next (Stop, Pcoq.G.Symbol.nterm vernac_control), act_vernac); ] in Pcoq.grammar_extend main_entry (None, [None, None, rule]) |