From 967883e29a46a0fff9da8e56974468531948b174 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 17:55:48 +0200
Subject: Add [Info] command.

Called with [Info n tac], runs [tac] and prints its info trace unfolding [n] level of tactic names ([0] for no unfolding at all).
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5cd34038f6..6cd56e6a63 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 *)
-- 
cgit v1.2.3