aboutsummaryrefslogtreecommitdiff
path: root/coqpp
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-02-25 09:42:18 +0100
committerPierre-Marie Pédrot2020-02-25 09:42:18 +0100
commitcb428dd8834747f6d5ea97b88bdef5a8f04495b8 (patch)
tree0cf0e2e0c75b50b101f1c41a6953e780ebc784af /coqpp
parentda984ceafbb450dc5a9fe8f8971d8c90a060f233 (diff)
parent4dd2102b7b12efb3ff7805aab3b7f318c6e3f989 (diff)
Merge PR #11655: [parsing] Track need to reinit by typing
Reviewed-by: ppedrot
Diffstat (limited to 'coqpp')
-rw-r--r--coqpp/coqpp_main.ml2
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 =