diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 11:28:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 15:16:10 +0200 |
| commit | df2d71323081f8a395881ffc0e1793e429abc3bb (patch) | |
| tree | 66e77810a4df69233c577c20732c06cdccf1d9db /ltac | |
| parent | 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c (diff) | |
Turning the grammar extend command API into a state-passing one.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 5c1e7c033..aedcb76eb 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -157,7 +157,7 @@ let rec prod_item_of_symbol lev = function (** Tactic grammar extensions *) -let add_tactic_entry (kn, ml, tg) = +let add_tactic_entry (kn, ml, tg) state = let open Tacexpr in let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = @@ -186,7 +186,7 @@ let add_tactic_entry (kn, ml, tg) = let rules = make_rule mkact prods in synchronize_level_positions (); grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - 1 + (1, state) let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry |