Fix deprecated warnings from Pcoq.

1 files changed, 22 insertions, 22 deletions

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 *)