diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 380bc501d..ac5046ef0 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -351,15 +351,13 @@ let check_evtags ?(tags : evtags option) (src : symbol list) =
       let dfl =
         not (List.mem explicit src) &&
         not (List.exists (fun (mode, _) -> mode = `Include) tags) in
-      let stt =
-        List.map (fun src ->
-          let do1 status (mode, dst) =
-            match mode with
-            | `Exclude -> if sym_equal src dst then raise Reject; status
-            | `Include -> status || (sym_equal src dst)
-          in List.fold_left do1 dfl tags)
-          src
-      in List.mem true stt
+      let has_tag dst = List.exists (fun s -> sym_equal s dst) src in
+      let do1 status (mode, dst) =
+        match mode with
+        | `Exclude -> if has_tag dst then raise Reject; status
+        | `Include -> status || has_tag dst
+      in
+      List.fold_left do1 dfl tags
 
   with Reject -> false
 
diff --git a/tests/clone-proofstar-tagdrop.ec b/tests/clone-proofstar-tagdrop.ec
new file mode 100644
index 000000000..ce57e736d
--- /dev/null
+++ b/tests/clone-proofstar-tagdrop.ec
@@ -0,0 +1,14 @@
+(* Regression for the clone `proof * [tag]` untagged-axiom drop.
+
+   Under a bracketed prove-all directive (`proof * [-dummy]`) the UNTAGGED
+   FinType.enum_spec axiom must still be FORCED. With `enum <- [0]` it is
+   false, so the discharging `by smt()` cannot prove it and the whole `clone`
+   command must fail. Before the fix the untagged axiom was silently dropped,
+   so this clone was accepted (and `F.enum_spec` could be used to prove
+   `false`). *)
+require import AllCore List FinType.
+
+fail clone FinType as F with
+  type t <- int,
+  op enum <- [0]
+  proof * [-dummy] by smt().