From 64637ffc5054199459d9fc7f07b84a99da71c6f1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 17:24:05 +0100
Subject: Removing "intro" from the tactic AST.

Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 4fe60538a4..0a0927b3fd 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -139,7 +139,6 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of 'dtrm intro_pattern_expr located list
-  | TacIntroMove of Id.t option * 'nam move_location
   | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
-- 
cgit v1.2.3