aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/vernacexpr.mli')
-rw-r--r--intf/vernacexpr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5cd34038f..6cd56e6a6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -350,7 +350,7 @@ type vernac_expr =
(* Solving *)
- | VernacSolve of goal_selector * raw_tactic_expr * bool
+ | VernacSolve of goal_selector * int option * raw_tactic_expr * bool
| VernacSolveExistential of int * constr_expr
(* Auxiliary file and library management *)