From 7d4a0bdbd18aba40a170bfd3eeb43c7f8ff12ecf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 6 Sep 2003 14:18:38 +0000
Subject: 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
---
 parsing/tacextend.ml4 | 4 ++--
 1 file 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
-- 
cgit v1.2.3