From e24c006e3d607239e88c1fe4e9dae7118f67a81c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 31 May 2016 17:05:28 +0200
Subject: [PATCH] solve_proper: let it prove pointwise_relation as well

---
 prelude/tactics.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index 98c88fe99..d299fe2f6 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
-- 
GitLab