diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 03:17:25 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 23:45:00 -0400 |
| commit | 767ecfec49543b70a605d20b1dae8252e1faabfe (patch) | |
| tree | 2b91f76b9f6c5148c7ba5e2b7cab14218d569259 /coqpp/coqpp_main.ml | |
| parent | 13929f39f8560cfcb3aacf20c84c6dcb5295cec5 (diff) | |
[parsing] Make grammar rules 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 'coqpp/coqpp_main.ml')
| -rw-r--r-- | coqpp/coqpp_main.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 5d1f0a876f..70e400c29b 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -217,13 +217,13 @@ let rec print_prod fmt p = and print_extrule fmt (tkn, vars, body) = let tkn = List.rev tkn in - fprintf fmt "@[Pcoq.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body) + fprintf fmt "@[Pcoq.G.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body) and print_symbols ~norec fmt = function -| [] -> fprintf fmt "Pcoq.Stop" +| [] -> fprintf fmt "Pcoq.G.Rule.stop" | tkn :: tkns -> - let c = if norec then "Pcoq.NextNoRec" else "Pcoq.Next" in - fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn + let c = if norec then "Pcoq.G.Rule.next_norec" else "Pcoq.G.Rule.next" in + fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> |