diff --git a/prelude/tactics.v b/prelude/tactics.v
index 98c88fe99693d909012237e02ba50dff5ae36f21..d299fe2f6579f83cb515150bb25ee4115e6f6930 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -316,6 +316,7 @@ Ltac solve_proper :=
   repeat lazymatch goal with
   | |- Proper _ _ => intros ???
   | |- (_ ==> _)%signature _ _ => intros ???
+  | |- pointwise_relation _ _ _ _ => intros ?
   end;
   (* Unfold the head symbol, which is the one we are proving a new property about *)
   lazymatch goal with