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

6 files changed, 22 insertions, 20 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index f5bf5e099..42d6354af 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
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c373371d2..bc6571b94 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -7,21 +7,21 @@
 (************************************************************************)
 
 open Pp
-open Pcoq
 open Errors
 open Util
 open Tacexpr
 open Genredexpr
-open Genarg
 open Constrexpr
 open Libnames
-open Termops
 open Tok
 open Compat
 open Misctypes
 open Locus
 open Decl_kinds
 
+open Pcoq
+
+
 let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta]
 
 let tactic_kw = [ "->"; "<-" ; "by" ]
@@ -121,7 +121,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
-    Errors.user_err_loc
+    user_err_loc
       (aloc,"Constr:mk_cofix_tac",
        Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
@@ -163,7 +163,8 @@ let rec mkCLambdaN_simple_loc loc bll c =
 let mkCLambdaN_simple bl c =
   if bl=[] then c
   else
-    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr.constr_loc c) in
+    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr
+.constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
 let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 51088564b..f7d80a074 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -17,8 +17,6 @@ open Topconstr
 open Extend
 open Vernacexpr
 open Locality
-open Pcoq
-open Tactic
 open Decl_kinds
 open Genarg
 open Ppextend
@@ -26,10 +24,12 @@ open Goptions
 open Declaremods
 open Misctypes
 
-open Prim
-open Constr
-open Vernac_
-open Module
+open Pcoq
+open Pcoq.Tactic
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Vernac_
+open Pcoq.Module
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
 let _ = List.iter Lexer.add_keyword vernac_kw
@@ -712,7 +712,11 @@ GEXTEND Gram
   GLOBAL: command check_command class_rawexpr;
 
   command:
-    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
+    [ [ IDENT "Ltac";
+        l = LIST1 tacdef_body SEP "with" ->
+          VernacDeclareTacticDefinition (use_module_locality (), true, l)
+
+      | IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
       (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 7ab65b443..1a9c03f72 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -71,7 +71,6 @@ Ppextend
 Tok
 Lexer
 Extend
-Locality
 Extrawit
 Pcoq
 Q_util
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ee241384b..ba3def1a0 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -406,6 +406,9 @@ module Tactic =
     (* Main entry for quotations *)
     let tactic_eoi = eoi_entry tactic
 
+    (* For Ltac definition *)
+    let tacdef_body = Gram.entry_create "tactic:tacdef_body"
+
   end
 
 module Vernac_ =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 886f91ea0..5d12af054 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -228,6 +228,7 @@ module Tactic :
     val binder_tactic : raw_tactic_expr Gram.entry
     val tactic : raw_tactic_expr Gram.entry
     val tactic_eoi : raw_tactic_expr Gram.entry
+    val tacdef_body : (reference * bool * raw_tactic_expr) Gram.entry
   end
 
 module Vernac_ :