aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-10 19:42:39 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-10 20:31:38 +0200
commitbc3981687cd363820e35e5a2bd037d50e213f524 (patch)
tree7829deffc40f17be0ef9ab423cad410e71ab6ac2 /parsing/pcoq.ml
parentb82512946a2818e13397b9f1a128fcafe4a78ba5 (diff)
Overlooked use of Gram instead of G module in Pcoq.
This was probably wreaking havoc in tricky undo-redo scenarii.
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8fa5da4bd..305cd4f80 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -572,7 +572,7 @@ let epsilon_value f e =
let r = Rule (Next (Stop, e), fun x _ -> f x) in
let ext = of_coq_extend_statement (None, [None, None, [r]]) in
let entry = G.entry_create "epsilon" in
- let () = maybe_uncurry (Gram.extend entry) ext in
+ let () = maybe_uncurry (G.extend entry) ext in
try Some (parse_string entry "") with _ -> None
(** Registering grammar of generic arguments *)