diff --git a/iris/proofmode/sel_patterns.v b/iris/proofmode/sel_patterns.v
index 6f498a36560fd998624152ebf123f497ff1bdfa2..4f74efe1bf419edd402361ffa0e741fff370d588 100644
--- a/iris/proofmode/sel_patterns.v
+++ b/iris/proofmode/sel_patterns.v
@@ -39,5 +39,6 @@ Ltac parse s :=
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid sel_pat" s
      end
+  | ?X => fail "sel_pat.parse:" s "has unexpected type" X
   end.
 End sel_pat.