Skip to content
Snippets Groups Projects
Commit 33f0447a authored by Ralf Jung's avatar Ralf Jung
Browse files

solve_proper: let it prove pointwise_relation as well

parent 49a61c0d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
theories/tactics.v
+ 1
− 0
View file @ 33f0447a
...@@ -316,6 +316,7 @@ Ltac solve_proper := ...@@ -316,6 +316,7 @@ Ltac solve_proper :=
repeat lazymatch goal with repeat lazymatch goal with
| |- Proper _ _ => intros ??? | |- Proper _ _ => intros ???
| |- (_ ==> _)%signature _ _ => intros ??? | |- (_ ==> _)%signature _ _ => intros ???
| |- pointwise_relation _ _ _ _ => intros ?
end; end;
(* Unfold the head symbol, which is the one we are proving a new property about *) (* Unfold the head symbol, which is the one we are proving a new property about *)
lazymatch goal with lazymatch goal with
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment