diff options
| -rw-r--r-- | parsing/tacextend.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index a7da88b52e..218a9e0db3 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -179,10 +179,10 @@ let declare_tactic loc s cl = try Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) with e -> Pp.pp (Cerrors.explain_exn e); - Egrammar.extend_tactic_grammar $se'$ $gl'$; + if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$ + else Egrammar.extend_tactic_grammar $se'$ $gl'$; let pp' = fun [ $list:pl'$ ] in Pptactic.declare_extra_tactic_pprule True $se'$ pp'; - Egrammar.extend_tactic_grammar $se'$ $gl$; let pp = fun [ $list:pl$ ] in Pptactic.declare_extra_tactic_pprule False $se'$ pp; end |