From 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Apr 2016 19:27:30 +0200
Subject: Removing "double induction" from the tactic AST.

---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e06436d8a3..4fe60538a4 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -157,7 +157,6 @@ type 'a gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
-  | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
   | TacRename of ('nam *'nam) list
-- 
cgit v1.2.3


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


From 5cd0310f061b5eb1a631a0fff0ee7eb9674a11c3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Apr 2016 14:13:14 +0200
Subject: Removing "exact" from the tactic AST.

---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0a0927b3fd..e1d4809609 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
-  | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
-- 
cgit v1.2.3


From 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 00:12:19 +0200
Subject: Removing "rename" from the tactic AST.

---
 intf/tacexpr.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e1d4809609..379dd59d39 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -156,9 +156,6 @@ type 'a gen_atomic_tactic_expr =
   | TacInductionDestruct of
       rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
 
-  (* Context management *)
-  | TacRename of ('nam *'nam) list
-
   (* Conversion *)
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
-- 
cgit v1.2.3