diff --git a/theories/tactics.v b/theories/tactics.v
index bfc7815689d4362fadb8ad4607a3b3f271dc9eae..8150d2d6c74b634a3aae2913e60775eb7f10bcbb 100644
--- a/theories/tactics.v
+++ b/theories/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