aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--grammar/coqpp_main.ml2
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--parsing/pcoq.mli2
3 files changed, 3 insertions, 3 deletions
diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml
index ef591bc99..e76a1e9ed 100644
--- a/grammar/coqpp_main.ml
+++ b/grammar/coqpp_main.ml
@@ -250,7 +250,7 @@ let print_rule fmt r =
let print_entry fmt gram 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 () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ "
+ fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ "
gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
let print_ast fmt ext =
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 171276a70..997ea78e6 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -336,7 +336,7 @@ module Gram =
I'm not entirely sure it makes sense, but at least it would be more correct.
*)
G.delete_rule e pil
- let safe_extend e ext = grammar_extend e None ext
+ let gram_extend e ext = grammar_extend e None ext
end
(** Remove extensions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 48604e188..154de1221 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,7 +80,7 @@ module type S =
(* Get comment parsing information from the Lexer *)
val comment_state : coq_parsable -> ((int * int) * string) list
- val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit
+ val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
(* Apparently not used *)
val srules' : production_rule list -> symbol