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.

---
 grammar/q_coqast.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 4fede761f4..1614301ec8 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -303,8 +303,6 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacIntroPattern pl ->
       let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in
       <:expr< Tacexpr.TacIntroPattern $pl$ >>
-  | Tacexpr.TacIntrosUntil h ->
-      <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacIntroMove (idopt,idopt') ->
       let idopt = mlexpr_of_ident_option idopt in
       let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in
-- 
cgit v1.2.3