aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Parmov.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Parmov.v')
-rw-r--r--lib/Parmov.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 92bba559..2d09171d 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -1564,7 +1564,7 @@ Proof.
subst. rewrite update_s. rewrite weak_update_s. apply H1.
destruct H. apply no_adherence_src; auto. apply no_adherence_tmp; auto.
rewrite update_o. rewrite weak_update_d. apply H1. auto.
- auto. apply sym_not_equal. apply disjoint_not_equal. auto.
+ auto. apply not_eq_sym. apply disjoint_not_equal. auto.
Qed.
Lemma weak_exec_seq_match: