- | node :: nodes ->
- if node_is_ready_to_run state node then (
- state.sorted_nodes <- List.rev acc @ nodes;
- match node with
- | Goal (env, loc, name, args, goal, extra_deps, debug_goal) ->
- Jobs.Job (node, fun () ->
- state.goal_runner env loc name args goal
- extra_deps debug_goal)
- | Exists (env, loc, p, debug_tactic) ->
- Jobs.Job (node, fun () ->
- state.exists_runner env loc p debug_tactic)
+ | node :: nodes when node_is_ready_to_run state node ->
+ (* Drop the node from the list of jobs and run it. *)
+ state.sorted_nodes <- List.rev acc @ nodes;
+ (match node with
+ | Goal (env, loc, name, args, goal, extra_deps, debug_goal) ->
+ Jobs.Job (node, fun () ->
+ state.goal_runner env loc name args goal
+ extra_deps debug_goal)
+ | Exists (env, loc, p, debug_pred) ->
+ Jobs.Job (node, fun () ->
+ state.exists_runner env loc p debug_pred)