From f3e611b2115b425f875e971ac9ff7534c2af2800 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Dec 2015 13:56:40 +0100
Subject: Separation of concern in TacAlias API.

The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
---
 intf/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 6d10ef9d51..05e7ea1a3b 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -294,7 +294,7 @@ and 'a gen_tactic_expr =
   (* For ML extensions *)
   | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)
-  | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list
+  | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list
 
 constraint 'a = <
     term:'t;
-- 
cgit v1.2.3