diff options
Diffstat (limited to 'parsing/q_coqast.ml4')
| -rw-r--r-- | parsing/q_coqast.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 1f352f6af..2b3967707 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -407,8 +407,9 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacLeft $mlexpr_of_binding_kind l$>> | Tacexpr.TacRight l -> <:expr< Tacexpr.TacRight $mlexpr_of_binding_kind l$>> - | Tacexpr.TacSplit l -> - <:expr< Tacexpr.TacSplit $mlexpr_of_binding_kind l$>> + | Tacexpr.TacSplit (b,l) -> + <:expr< Tacexpr.TacSplit + ($mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>> | Tacexpr.TacAnyConstructor t -> <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_option mlexpr_of_tactic t$>> | Tacexpr.TacConstructor (n,l) -> |