Fix deprecated warnings from Pcoq.

3 files changed, 51 insertions, 51 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 16e7278235..82ab53298e 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -81,14 +81,14 @@ let test_dollar_ident =
   end
 
 let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Gram.entry_create "tactic:tac2type"
-let tac2def_val = Gram.entry_create "tactic:tac2def_val"
-let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
-let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
-let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
-let tac2def_mut = Gram.entry_create "tactic:tac2def_mut"
-let tac2def_run = Gram.entry_create "tactic:tac2def_run"
-let tac2mode = Gram.entry_create "vernac:ltac2_command"
+let tac2type = Entry.create "tactic:tac2type"
+let tac2def_val = Entry.create "tactic:tac2def_val"
+let tac2def_typ = Entry.create "tactic:tac2def_typ"
+let tac2def_ext = Entry.create "tactic:tac2def_ext"
+let tac2def_syn = Entry.create "tactic:tac2def_syn"
+let tac2def_mut = Entry.create "tactic:tac2def_mut"
+let tac2def_run = Entry.create "tactic:tac2def_run"
+let tac2mode = Entry.create "vernac:ltac2_command"
 
 let ltac1_expr = Pltac.tactic_expr
 
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 8ebfeec948..c26fbdc478 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -22,28 +22,28 @@ open Tac2intern
 
 module Pltac =
 struct
-let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
-
-let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
-let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
-let q_with_bindings = Pcoq.Gram.entry_create "tactic:q_with_bindings"
-let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
-let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
-let q_destruction_arg = Pcoq.Gram.entry_create "tactic:q_destruction_arg"
-let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
-let q_conversion = Pcoq.Gram.entry_create "tactic:q_conversion"
-let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
-let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
-let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
-let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
-let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
-let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
-let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
-let q_goal_matching = Pcoq.Gram.entry_create "tactic:q_goal_matching"
-let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
-let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
-let q_pose = Pcoq.Gram.entry_create "tactic:q_pose"
-let q_assert = Pcoq.Gram.entry_create "tactic:q_assert"
+let tac2expr = Pcoq.Entry.create "tactic:tac2expr"
+
+let q_ident = Pcoq.Entry.create "tactic:q_ident"
+let q_bindings = Pcoq.Entry.create "tactic:q_bindings"
+let q_with_bindings = Pcoq.Entry.create "tactic:q_with_bindings"
+let q_intropattern = Pcoq.Entry.create "tactic:q_intropattern"
+let q_intropatterns = Pcoq.Entry.create "tactic:q_intropatterns"
+let q_destruction_arg = Pcoq.Entry.create "tactic:q_destruction_arg"
+let q_induction_clause = Pcoq.Entry.create "tactic:q_induction_clause"
+let q_conversion = Pcoq.Entry.create "tactic:q_conversion"
+let q_rewriting = Pcoq.Entry.create "tactic:q_rewriting"
+let q_clause = Pcoq.Entry.create "tactic:q_clause"
+let q_dispatch = Pcoq.Entry.create "tactic:q_dispatch"
+let q_occurrences = Pcoq.Entry.create "tactic:q_occurrences"
+let q_reference = Pcoq.Entry.create "tactic:q_reference"
+let q_strategy_flag = Pcoq.Entry.create "tactic:q_strategy_flag"
+let q_constr_matching = Pcoq.Entry.create "tactic:q_constr_matching"
+let q_goal_matching = Pcoq.Entry.create "tactic:q_goal_matching"
+let q_hintdb = Pcoq.Entry.create "tactic:q_hintdb"
+let q_move_location = Pcoq.Entry.create "tactic:q_move_location"
+let q_pose = Pcoq.Entry.create "tactic:q_pose"
+let q_assert = Pcoq.Entry.create "tactic:q_assert"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 37944981d7..f97e35fec0 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -56,32 +56,32 @@ val backtrace : backtrace Exninfo.t
 
 module Pltac :
 sig
-val tac2expr : raw_tacexpr Pcoq.Gram.entry
+val tac2expr : raw_tacexpr Pcoq.Entry.t
 
 (** Quoted entries. To be used for complex notations. *)
 
 open Tac2qexpr
 
-val q_ident : Id.t CAst.t or_anti Pcoq.Gram.entry
-val q_bindings : bindings Pcoq.Gram.entry
-val q_with_bindings : bindings Pcoq.Gram.entry
-val q_intropattern : intro_pattern Pcoq.Gram.entry
-val q_intropatterns : intro_pattern list CAst.t Pcoq.Gram.entry
-val q_destruction_arg : destruction_arg Pcoq.Gram.entry
-val q_induction_clause : induction_clause Pcoq.Gram.entry
-val q_conversion : conversion Pcoq.Gram.entry
-val q_rewriting : rewriting Pcoq.Gram.entry
-val q_clause : clause Pcoq.Gram.entry
-val q_dispatch : dispatch Pcoq.Gram.entry
-val q_occurrences : occurrences Pcoq.Gram.entry
-val q_reference : reference or_anti Pcoq.Gram.entry
-val q_strategy_flag : strategy_flag Pcoq.Gram.entry
-val q_constr_matching : constr_matching Pcoq.Gram.entry
-val q_goal_matching : goal_matching Pcoq.Gram.entry
-val q_hintdb : hintdb Pcoq.Gram.entry
-val q_move_location : move_location Pcoq.Gram.entry
-val q_pose : pose Pcoq.Gram.entry
-val q_assert : assertion Pcoq.Gram.entry
+val q_ident : Id.t CAst.t or_anti Pcoq.Entry.t
+val q_bindings : bindings Pcoq.Entry.t
+val q_with_bindings : bindings Pcoq.Entry.t
+val q_intropattern : intro_pattern Pcoq.Entry.t
+val q_intropatterns : intro_pattern list CAst.t Pcoq.Entry.t
+val q_destruction_arg : destruction_arg Pcoq.Entry.t
+val q_induction_clause : induction_clause Pcoq.Entry.t
+val q_conversion : conversion Pcoq.Entry.t
+val q_rewriting : rewriting Pcoq.Entry.t
+val q_clause : clause Pcoq.Entry.t
+val q_dispatch : dispatch Pcoq.Entry.t
+val q_occurrences : occurrences Pcoq.Entry.t
+val q_reference : reference or_anti Pcoq.Entry.t
+val q_strategy_flag : strategy_flag Pcoq.Entry.t
+val q_constr_matching : constr_matching Pcoq.Entry.t
+val q_goal_matching : goal_matching Pcoq.Entry.t
+val q_hintdb : hintdb Pcoq.Entry.t
+val q_move_location : move_location Pcoq.Entry.t
+val q_pose : pose Pcoq.Entry.t
+val q_assert : assertion Pcoq.Entry.t
 end
 
 (** {5 Hooks} *)