From b600c51753c5b60e62bdfcf1e6409afa1ce69d7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Aug 2014 01:10:26 +0200
Subject: Removing "intros untils" from the AST.

---
 parsing/g_tactic.ml4 | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3c097db1ce..29cb45ad19 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -528,9 +528,7 @@ GEXTEND Gram
   simple_tactic:
     [ [
       (* Basic tactics *)
-        IDENT "intros"; IDENT "until"; id = quantified_hypothesis ->
-	  TacIntrosUntil id
-      | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
+        IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
       | IDENT "intro"; id = ident; hto = move_location ->
 	  TacIntroMove (Some id, hto)
       | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto)
-- 
cgit v1.2.3