From f7198dfc6a473781b429871cb098325c1b8ce331 Mon Sep 17 00:00:00 2001
From: "Richard W.M. Jones" <rjones@redhat.com>
Date: Fri, 3 Jan 2020 07:54:11 +0000
Subject: [PATCH] eval: If multiple goals match a tactic, run them all.

---
 src/ast.mli |  5 ++---
 src/eval.ml | 15 +++++++--------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/ast.mli b/src/ast.mli
index b42294c..406a829 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -113,9 +113,8 @@ module Substs : sig
   val add_var : t -> string -> unit
 end
 
-(** Print all definitions in an environment. *)
-val print_env : out_channel -> env -> unit
-
 (** %a formatters. *)
+val print_env : out_channel -> env -> unit
 val string_pattern : unit -> pattern -> string
 val string_expr : unit -> expr -> string
+val print_expr : out_channel -> expr -> unit
diff --git a/src/eval.ml b/src/eval.ml
index 8ab2d5f..1520dcb 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -243,9 +243,6 @@ and run_tactic env loc tactic cargs =
     ) patterns in
 
   match patterns with
-  | [_, name, goal, args] ->
-     run_goal env loc name args goal
-
   | [] ->
      (* There's no matching goal, but we don't need one if
       * the tactic doesn't need to be rebuilt.
@@ -260,12 +257,14 @@ and run_tactic env loc tactic cargs =
          Ast.string_loc loc Ast.string_expr t
      )
 
-  | _ ->
-     (* If there are multiple matching goals, then assuming the goals
-      * are different we must pick the one which was defined last in
-      * the file.  However we don't do that right now. XXX
+  | goals ->
+     (* One or more goals match.  We run them all (although if
+      * one of them succeeds in rebuilding, it will cut short the rest).
       *)
-     assert false (* TODO! *)
+     List.iter (
+       fun (_, name, goal, args) ->
+         run_goal env loc name args goal
+     ) goals
 
 (* Test if pattern matches *tactic(cargs).  If it does
  * then we return Some args where args is the arguments that must
-- 
1.8.3.1