aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-07 17:46:53 +0200
committerPierre-Marie Pédrot2016-09-07 17:46:53 +0200
commit79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (patch)
tree92ce430c64b7bea374b926d81acc5433d39fdcbb /parsing
parentf79f2b32da8e5e443428d4f642216ddfb404857c (diff)
parenta18fb93587ccbe32a2edfad38d2e9095f6c8e901 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'parsing')
-rw-r--r--parsing/pcoq.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 0e74e6f0c1..714e25f85e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -132,13 +132,13 @@ let grammar_delete e reinit (pos,rls) =
let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
let undo () = grammar_delete e reinit ext in
- let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in
+ let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in
camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
redo ()
let grammar_extend_sync e reinit ext =
camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
- camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext)
+ camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext)
(** The apparent parser of Coq; encapsulate G to keep track
of the extensions. *)