From 07723dc27b9878109b8df7799def7058494f019b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 14:10:38 +0200
Subject: [PATCH] Use congruence in wp_cas_fail and wp_cas_suc.
---
heap_lang/proofmode.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 1f6b56802..086fdd294 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -155,7 +155,7 @@ Tactic Notation "wp_cas_fail" :=
|done || eauto with ndisj
|apply _
|iAssumptionCore || fail 2 "wp_cas_fail: cannot find" l "↦ ?"
- |try discriminate
+ |try congruence
|wp_finish]
end) || fail "wp_cas_fail: cannot find 'CAS' in" e
| _ => fail "wp_cas_fail: not a 'wp'"
@@ -173,7 +173,7 @@ Tactic Notation "wp_cas_suc" :=
|done || eauto with ndisj
|apply _
|iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
- |try reflexivity
+ |try congruence
|env_cbv; reflexivity
|wp_finish]
end) || fail "wp_cas_suc: cannot find 'CAS' in" e
--
GitLab