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