Commit 07723dc2 authored by Robbert Krebbers's avatar Robbert Krebbers

Use congruence in wp_cas_fail and wp_cas_suc.

parent 27baa1d5
...@@ -155,7 +155,7 @@ Tactic Notation "wp_cas_fail" := ...@@ -155,7 +155,7 @@ Tactic Notation "wp_cas_fail" :=
|done || eauto with ndisj |done || eauto with ndisj
|apply _ |apply _
|iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?" |iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
|try discriminate |try congruence
|wp_finish] |wp_finish]
end) || fail "wp_cas_fail: cannot find 'CAS' in" e end) || fail "wp_cas_fail: cannot find 'CAS' in" e
| _ => fail "wp_cas_fail: not a 'wp'" | _ => fail "wp_cas_fail: not a 'wp'"
...@@ -173,7 +173,7 @@ Tactic Notation "wp_cas_suc" := ...@@ -173,7 +173,7 @@ Tactic Notation "wp_cas_suc" :=
|done || eauto with ndisj |done || eauto with ndisj
|apply _ |apply _
|iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?" |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
|try reflexivity |try congruence
|env_cbv; reflexivity |env_cbv; reflexivity
|wp_finish] |wp_finish]
end) || fail "wp_cas_suc: cannot find 'CAS' in" e end) || fail "wp_cas_suc: cannot find 'CAS' in" e
......
Markdown is supported
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