aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/xlate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/xlate.ml')
-rw-r--r--contrib/interface/xlate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c9079a8fc1..2ceb5789c6 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1223,7 +1223,7 @@ let xlate_vernac =
| VernacAbort None -> CT_abort ctv_ID_OPT_OR_ALL_NONE
| VernacAbortAll -> CT_abort ctv_ID_OPT_OR_ALL_ALL
| VernacRestart -> CT_restart
- | VernacSolve (n, tac) -> CT_solve (CT_int n, xlate_tactic tac)
+ | VernacSolve (n, tac, b) -> CT_solve (CT_int n, xlate_tactic tac)
| VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
| VernacUnfocus -> CT_unfocus
| VernacExtend ("HintRewrite", orient :: formula_list :: base :: t) ->