From 16d0e6f7cfc453944874cc1665a0eb4db8ded354 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 15:33:47 +0200
Subject: Making the grammar command extend API purely functional.

Instead of leaving the responsibility of extending the grammar to the caller,
we ask for a list of extensions in the return value of the function.
---
 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 714bfa8417..5720a6f378 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -184,8 +184,8 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
-  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
-  (1, state)
+  let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in
+  ([r], state)
 
 let tactic_grammar =
   create_grammar_command "TacticGrammar" add_tactic_entry
-- 
cgit v1.2.3