solve_proper: let it prove pointwise_relation as well

e24c006e · Ralf Jung · 173af5fb · e24c006e
Commit e24c006e authored May 31, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

prelude/tactics.v prelude/tactics.v +1 -0

No files found.
--- 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