diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 2a6cac32110db49e9e4a119ca2b392904c8ce71e..39a28f98b8a6c7772a7f31ecc1e67535ffea57e1 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -144,6 +144,9 @@ Fixpoint intro_pat_persistent (p : intro_pat) :=
   | IPureElim => true
   | IAlwaysElim _ => true
   | IList pps => forallb (forallb intro_pat_persistent) pps
+  | ISimpl => true
+  | IClear _ => true
+  | IClearFrame _ => true
   | _ => false
   end.