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.

---
 printing/pptactic.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 44c832bd7a..5192e2db12 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -909,12 +909,6 @@ module Make
                 pr_opt (pr_clauses None pr.pr_name) cl) l ++
               pr_opt pr_eliminator el
           )
-        | TacDoubleInduction (h1,h2) ->
-          hov 1 (
-            primitive "double induction"
-            ++ pr_arg pr_quantified_hypothesis h1
-            ++ pr_arg pr_quantified_hypothesis h2
-          )
 
         (* Context management *)
         | TacRename l ->
-- 
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.
---
 printing/pptactic.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5192e2db12..e4d155499b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -816,7 +816,6 @@ module Make
       (* Printing tactics as arguments *)
       let rec pr_atom0 a = tag_atom a (match a with
         | TacIntroPattern [] -> primitive "intros"
-        | TacIntroMove (None,MoveLast) -> primitive "intro"
         | t -> str "(" ++ pr_atom1 t ++ str ")"
       )
 
@@ -828,13 +827,6 @@ module Make
         | TacIntroPattern (_::_ as p) ->
           hov 1 (primitive "intros" ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-        | TacIntroMove (None,MoveLast) as t ->
-          pr_atom0 t
-        | TacIntroMove (Some id,MoveLast) ->
-          primitive "intro" ++ spc () ++ pr_id id
-        | TacIntroMove (ido,hto) ->
-          hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
-                    Miscprint.pr_move_location pr.pr_name hto)
         | TacExact c ->
           hov 1 (primitive "exact" ++ pr_constrarg c)
         | TacApply (a,ev,cb,inhyp) ->
-- 
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.

---
 printing/pptactic.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e4d155499b..633ff18762 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -827,8 +827,6 @@ module Make
         | TacIntroPattern (_::_ as p) ->
           hov 1 (primitive "intros" ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-        | TacExact c ->
-          hov 1 (primitive "exact" ++ pr_constrarg c)
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
             (if a then mt() else primitive "simple ") ++
-- 
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.

---
 printing/pptactic.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 633ff18762..114410fed1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -900,17 +900,6 @@ module Make
               pr_opt pr_eliminator el
           )
 
-        (* Context management *)
-        | TacRename l ->
-          hov 1 (
-            primitive "rename" ++ brk (1,1)
-            ++ prlist_with_sep
-              (fun () -> str "," ++ brk (1,1))
-              (fun (i1,i2) ->
-                pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-              l
-          )
-
         (* Conversion *)
         | TacReduce (r,h) ->
           hov 1 (
-- 
cgit v1.2.3