X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Frun.mli;h=ec26096c3b1a8da38be68b3b4092b030e99c5fd1;hb=a70987f316ab4b948bf941ddea8fb6ccef09da4f;hp=4251235247f41a9400e2a9dba9bfc2330467a948;hpb=0aead2922062dc8a4e7dc88fe7776f92ac6c232a;p=goals.git

diff --git a/src/run.mli b/src/run.mli
index 4251235..ec26096 100644
--- a/src/run.mli
+++ b/src/run.mli
@@ -17,12 +17,15 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-val run_targets_to_completion : Ast.env -> Ast.expr list -> unit
-(** This drives evaluation of the list of target expressions (in
-    parallel) until they are complete or we reach an error.  The
-    expressions are either a list of dependencies and/or a list of
-    initial targets. *)
+val goal_runner : Deps.goal_runner
+(** Run a single goal. *)
 
-val stop_all : unit -> unit
-(** Wait until all running jobs finish, and don't start any new ones.
-    See [Jobs.stop_all]. *)
+val exists_runner : Deps.exists_runner
+(** Run the implicit existence tactic.
+
+    This is used when we find a tactic like *foo(...) but there
+    is no matching goal.  We run (in this callback) the associated
+    tactic code.  As long as it runs successfully, not returning 99 or
+    any error value, then we're OK - the tactic doesn't need rebuilding
+    so the dependency is satisfied.  However if it returns 99 (needs
+    rebuild) or an error then we have to exit with an error. *)