diff options
| author | Arnaud Spiwack | 2014-08-05 17:55:48 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 967883e29a46a0fff9da8e56974468531948b174 (patch) | |
| tree | 9c9a814a92c2a7fb5006d478e6d20e16bcf74d7a /stm | |
| parent | 3c8797a7e0d6536e28b8a8e7f4256241fc79dfc8 (diff) | |
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).
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4b4d50c41d..b72b5bb2a1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1125,7 +1125,7 @@ module Partac = struct let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = let e, etac, time, fail = - let rec find time fail = function VernacSolve(_,re,b) -> re, b, time, fail + let rec find time fail = function VernacSolve(_,_,re,b) -> re, b, time, fail | VernacTime [_,e] -> find true fail e | VernacFail e -> find time true e | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in @@ -1137,7 +1137,7 @@ module Partac = struct let open SubTask in let res = CList.map_i (fun i g -> let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in - let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,e,etac) } in + let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in let t_name = Goal.uid g in TaskQueue.enqueue_task { t_state = safe_id; t_state_fb = id; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 733f3e4412..63b9e2e7f5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -97,7 +97,7 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_) -> VtProofStep true, VtLater + | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus |