diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 15:35:13 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:09:29 -0500 |
| commit | 4dd2102b7b12efb3ff7805aab3b7f318c6e3f989 (patch) | |
| tree | 1c325b75c69fd8a4f8e8fff9c4fce9125c3fdbb1 /coqpp | |
| parent | e1f2a1b97bb61e9c5ebaffda55a3be1ea3267c6b (diff) | |
[parsing] Track need to reinit by typing
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_main.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 72b7cb2f84..e723d4ea1b 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -266,7 +266,7 @@ let print_rule fmt r = let print_entry fmt e = let print_position_opt fmt pos = print_opt fmt print_position pos in let print_rules fmt rules = print_list fmt print_rule rules in - fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ " + fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ " e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules let print_ast fmt ext = |