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..719acb15c
--- /dev/null
+++ b/tests/clone-proofstar-tagdrop.ec
@@ -0,0 +1,19 @@
+(* Regression for `proof * [-tag]` failing to force untagged axioms.
+
+   An exclusion-only bracket list (`proof * [-foo]`) means "force every axiom
+   except those tagged `foo`", so the untagged axiom `A` must be FORCED into a
+   proof obligation. `A` is unprovable, so the discharging tactic fails and
+   the whole `clone` command must fail. Before the fix the untagged axiom was
+   silently kept as an assumed axiom in the clone, so this clone was accepted
+   (and `U.A` could be used to prove `false`). *)
+require import AllCore.
+
+theory T.
+  axiom A : false.
+end T.
+
+fail clone T as U proof * [-foo] by done.
+
+(* An include list (`proof * [foo]`) forces ONLY the axioms tagged `foo`:
+   the untagged `A` is intentionally not forced and stays an axiom. *)
+clone T as V proof * [foo] by done.