From 44d0a3fb1b24561cfdf0eed6e331d450e152bbe4 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:56 +0000
Subject: Migrate the grammar entry about "Ltac" into g_vernac.ml4.

 It's the right place for it, and it will allow cutting some deps
 for grammar.cma later.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15378 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_ltac.ml4 | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'parsing/g_ltac.ml4')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index f5bf5e099c..42d6354afe 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -10,7 +10,6 @@ open Pp
 open Constrexpr
 open Tacexpr
 open Vernacexpr
-open Locality
 open Misctypes
 open Genredexpr
 
@@ -27,7 +26,7 @@ let arg_of_expr = function
 (* Tactics grammar rules *)
 
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
+  GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
           constr_may_eval;
 
   tactic_then_last:
@@ -223,9 +222,4 @@ GEXTEND Gram
   tactic:
     [ [ tac = tactic_expr -> tac ] ]
   ;
-  Vernac_.command:
-    [ [ IDENT "Ltac";
-        l = LIST1 tacdef_body SEP "with" ->
-          VernacDeclareTacticDefinition (use_module_locality (), true, l) ] ]
-  ;
   END
-- 
cgit v1.2.3