diff options
| -rw-r--r-- | src/g_ltac2.ml4 | 16 | ||||
| -rw-r--r-- | src/tac2entries.ml | 44 | ||||
| -rw-r--r-- | src/tac2entries.mli | 42 |
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} *) |