diff options
Diffstat (limited to 'grammar/q_coqast.ml4')
| -rw-r--r-- | grammar/q_coqast.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 4fede761f..1614301ec 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 |