diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:18:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 14:18:38 +0000 |
| commit | 7d4a0bdbd18aba40a170bfd3eeb43c7f8ff12ecf (patch) | |
| tree | 3cdded97f4806f7f81e6b2eace6b9bc208caa7be | |
| parent | cb8db3f7af710970a4ddba2fc559910ff7feaffb (diff) | |
Adapter l'entree de grammaire a la version 7 ou 8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4317 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 a7da88b52..218a9e0db 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 |