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.
---
 parsing/g_tactic.ml4 | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9f19817ddf..993695fb92 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,11 +528,6 @@ GEXTEND Gram
           TacAtom (!@loc, TacIntroPattern pl)
       | IDENT "intros" ->
           TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
-      | IDENT "intro"; id = ident; hto = move_location ->
-	  TacAtom (!@loc, TacIntroMove (Some id, hto))
-      | IDENT "intro"; hto = move_location -> TacAtom (!@loc, TacIntroMove (None, hto))
-      | IDENT "intro"; id = ident -> TacAtom (!@loc, TacIntroMove (Some id, MoveLast))
-      | IDENT "intro" -> TacAtom (!@loc, TacIntroMove (None, MoveLast))
 
       | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
 
-- 
cgit v1.2.3