diff options
| author | Pierre-Marie Pédrot | 2014-08-06 01:10:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-06 02:10:38 +0200 |
| commit | b600c51753c5b60e62bdfcf1e6409afa1ce69d7a (patch) | |
| tree | 025367115bb871a5c04b3317125b3677e003cf22 /grammar | |
| parent | dd37aea05fd568c98eb4d3970183c3dce1c23712 (diff) | |
Removing "intros untils" from the AST.
Diffstat (limited to 'grammar')
| -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 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 |