8 files changed, 9 insertions, 13 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4c4e51ecc..156ee94a66 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -332,7 +332,7 @@ END
 
 let local_test_lpar_id_colon =
   let err () = raise Stream.Failure in
-  Pcoq.Gram.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       match Util.stream_nth 0 strm with
         | Tok.KEYWORD "(" ->
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd8a097154..338839ee96 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -70,7 +70,7 @@ let _ =
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
+  Pcoq.Entry.of_parser "test_bracket_ident"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "[" ->
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index e29f78af5b..ef18dd6cdc 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -45,7 +45,6 @@ let with_tac f tac =
  * Subtac. These entries are named Subtac.<foo>
  *)
 
-module Gram = Pcoq.Gram
 module Tactic = Pltac
 
 open Pcoq
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2596bc22f2..f7375a0f01 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -226,8 +226,6 @@ let () =
   let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
   Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
 
-open Pcoq
-
 }
 
 GRAMMAR EXTEND Gram
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 0ce0fbd0cd..46ea3819ac 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -39,7 +39,7 @@ let err () = raise Stream.Failure
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let test_lpar_id_coloneq =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -53,7 +53,7 @@ let test_lpar_id_coloneq =
 
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
-  Gram.Entry.of_parser "lpar_id_coloneq"
+  Pcoq.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -67,7 +67,7 @@ let test_lpar_id_rpar =
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
-  Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+  Pcoq.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
       match stream_nth 0 strm with
         | KEYWORD "(" ->
@@ -84,7 +84,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Gram.Entry.of_parser "lpar_id_colon"
+  Pcoq.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       let rec skip_to_rpar p n =
 	match List.last (Stream.npeek n strm) with
@@ -108,7 +108,7 @@ let check_for_coloneq =
       | _ -> err ())
 
 let lookup_at_as_comma =
-  Gram.Entry.of_parser "lookup_at_as_comma"
+  Pcoq.Entry.of_parser "lookup_at_as_comma"
     (fun strm ->
       match stream_nth 0 strm with
 	| KEYWORD (","|"at"|"as") -> ()
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/plugin_base.dune
index 1b31655310..5611f5ba16 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/plugin_base.dune
@@ -3,7 +3,6 @@
  (public_name coq.plugins.ltac)
  (synopsis "Coq's LTAC tactic language")
  (modules :standard \ tauto)
- (flags :standard -open Gramlib)
  (libraries coq.stm))
 
 (library
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 188d5de7de..ac2d88dec2 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -697,7 +697,7 @@ type ('b, 'c) argument_interp =
 | ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
 | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
 | ArgInterpLegacy :
-  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+  (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
   arg_parsing : 'a Vernacextend.argument_rule;
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 79f9e093fb..309db539d0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -125,7 +125,7 @@ type ('b, 'c) argument_interp =
 | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
 | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
 | ArgInterpLegacy :
-  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+  (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
 
 type ('a, 'b, 'c) tactic_argument = {
   arg_parsing : 'a Vernacextend.argument_rule;