From 9a7da63b880cbeb3e58af5b2e0b39afcd650c253 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 30 Sep 2010 18:45:31 +0000
Subject: Simplify tactic(_)-bound arguments in TACTIC EXTEND rules

Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
component is kept, the second one can be obtained with
Tacinterp.eval_tactic.

Rationale: these declare parsing rules, and eval_tactic is a semantic
action, and therefore should be done in the rule body
instead. Moreover, having the glob_tactic_expr and its evaluation
captured by these rules was quite confusing IMHO.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/changes.txt | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 4617f4dee4..3953623885 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -13,6 +13,13 @@ efficiency, when an evar is known to be undefined, it is preferable to
 use specific functions about undefined evars since these ones are
 generally fewer than the defined ones.
 
+** Type changes in TACTIC EXTEND rules **
+
+Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
+glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
+component is kept, the second one can be obtained via
+Tacinterp.eval_tactic.
+
 =========================================
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
-- 
cgit v1.2.3