From df2d71323081f8a395881ffc0e1793e429abc3bb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 11 May 2016 11:28:04 +0200
Subject: Turning the grammar extend command API into a state-passing one.

---
 ltac/tacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ltac')

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
-- 
cgit v1.2.3