mirror of
https://github.com/achlipala/frap.git
synced 2025-03-14 17:21:46 +00:00
Beef up [equality]
This commit is contained in:
parent
3ae5327314
commit
44696bb5b1
1 changed files with 1 additions and 1 deletions
2
Frap.v
2
Frap.v
|
@ -62,7 +62,7 @@ Ltac linear_arithmetic := intros;
|
||||||
rewrite Heq in *; clear Heq
|
rewrite Heq in *; clear Heq
|
||||||
end; omega.
|
end; omega.
|
||||||
|
|
||||||
Ltac equality := congruence.
|
Ltac equality := intuition congruence.
|
||||||
|
|
||||||
Ltac cases E :=
|
Ltac cases E :=
|
||||||
((is_var E; destruct E)
|
((is_var E; destruct E)
|
||||||
|
|
Loading…
Add table
Reference in a new issue