Move Ltac-specific components from G_proofs to G_ltac.

2 files changed, 21 insertions, 14 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 42276ad3f..7fdfc452d 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -19,6 +19,7 @@ open Genredexpr
 open Tok (* necessary for camlp4 *)
 
 open Pcoq
+open Pcoq.Vernac_
 open Pcoq.Prim
 open Pcoq.Tactic
 
@@ -32,6 +33,7 @@ let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
 let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
+let in_tac tac = in_gen (rawwit Constrarg.wit_ltac) tac
 
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
@@ -72,13 +74,15 @@ let test_bracket_ident =
 
 (* Tactics grammar rules *)
 
+let hint = G_proofs.hint
+
 let warn_deprecated_appcontext =
   CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated"
          (fun () -> strbrk "appcontext is deprecated and will be removed " ++
                       strbrk "in a future version")
 
 GEXTEND Gram
-  GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
+  GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
           tactic_mode constr_may_eval constr_eval selector toplevel_selector;
 
   tactic_then_last:
@@ -327,6 +331,19 @@ GEXTEND Gram
   tactic_mode:
     [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ]
   ;
+  command:
+    [ [ IDENT "Proof"; "with"; ta = Pcoq.Tactic.tactic; 
+        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
+          Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
+      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
+        ta = OPT [ "with"; ta = Pcoq.Tactic.tactic -> in_tac ta ] ->
+          Vernacexpr.VernacProof (ta,Some l) ] ]
+  ;
+  hint:
+    [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
+        tac = Pcoq.Tactic.tactic ->
+          Vernacexpr.HintsExtern (n,c, in_tac tac) ] ]
+  ;
   END
 
 open Constrarg
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 6ce7ca023..2adbf300e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -13,7 +13,6 @@ open Misctypes
 open Tok
 
 open Pcoq
-open Pcoq.Tactic
 open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Vernac_
@@ -26,11 +25,11 @@ let hint_proof_using e = function
      | None -> None
      | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s)))
 
-let in_tac tac = Genarg.in_gen (Genarg.rawwit Constrarg.wit_ltac) tac
+let hint = Gram.entry_create "hint"
 
 (* Proof commands *)
 GEXTEND Gram
-  GLOBAL: command;
+  GLOBAL: hint command;
 
   opt_hintbases:
   [ [ -> []
@@ -41,12 +40,6 @@ GEXTEND Gram
       | IDENT "Proof" ->
           VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
-      | IDENT "Proof"; "with"; ta = tactic; 
-        l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
-          VernacProof (Some (in_tac ta),hint_proof_using G_vernac.section_subset_expr l)
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = tactic -> in_tac ta ] ->
-          VernacProof (ta,Some l)
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Abort" -> VernacAbort None
       | IDENT "Abort"; IDENT "All" -> VernacAbortAll
@@ -126,10 +119,7 @@ GEXTEND Gram
       | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
       | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m)
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
-      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
-      | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
-          tac = tactic ->
-	  HintsExtern (n,c, in_tac tac) ] ]
+      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ]
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c