From 48327426b59144f1a7181092068077c5a6df7c60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 10:45:31 +0100
Subject: Moving the "fix" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 502f2db4c1..3993f1b371 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -145,7 +145,6 @@ type 'a gen_atomic_tactic_expr =
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
-  | TacFix of Id.t option * int
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
-- 
cgit v1.2.3


From bda8b2e8f90235ca875422f211cb781068b20b3c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 10:54:08 +0100
Subject: Moving the "cofix" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3993f1b371..33a96150c1 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -146,7 +146,6 @@ type 'a gen_atomic_tactic_expr =
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
-  | TacCofix of Id.t option
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
       bool * 'tacexpr option *
-- 
cgit v1.2.3


From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 11:05:26 +0100
Subject: Moving the "clear" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 33a96150c1..10c616627a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacClear of bool * 'nam list
   | TacClearBody of 'nam list
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
-- 
cgit v1.2.3


From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 11:20:26 +0100
Subject: Moving the "clearbody" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 10c616627a..d936748f2d 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacClearBody of 'nam list
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
-- 
cgit v1.2.3


From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 11:35:34 +0100
Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d936748f2d..52c07e089a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -151,7 +151,6 @@ type 'a gen_atomic_tactic_expr =
       bool * 'tacexpr option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
-  | TacGeneralizeDep of 'trm
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
       intro_pattern_naming_expr located option
 
-- 
cgit v1.2.3


From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 12:11:52 +0100
Subject: Moving the "symmetry" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 52c07e089a..3f1d0fd76c 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -170,9 +170,6 @@ type 'a gen_atomic_tactic_expr =
   | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
   | TacChange of 'pat option * 'dtrm * 'nam clause_expr
 
-  (* Equivalence relations *)
-  | TacSymmetry of 'nam clause_expr
-
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
       (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
-- 
cgit v1.2.3


From 293222e49ff81bc1299b3822d2a8c526ca803307 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 12:40:45 +0100
Subject: Moving the "exists" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 3f1d0fd76c..dae960e0e5 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -163,9 +163,6 @@ type 'a gen_atomic_tactic_expr =
   | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
-  (* Trmuctors *)
-  | TacSplit of evars_flag * 'trm bindings 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


From 1397f791b1699b0f04d971465270d5b2df9a6d7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 13:32:39 +0100
Subject: Moving the "move" tactic to TACTIC EXTEND.

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

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index dae960e0e5..7366bc03e6 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -160,7 +160,6 @@ type 'a gen_atomic_tactic_expr =
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
 
   (* Context management *)
-  | TacMove of 'nam * 'nam move_location
   | TacRename of ('nam *'nam) list
 
   (* Conversion *)
-- 
cgit v1.2.3