From 1d937ab30d6cf86ca6296a4e13270f65affd300f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 2 Oct 2021 11:03:12 -0400
Subject: [PATCH] make f_contractive consistent with f_equiv
---
iris/algebra/ofe.v | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index df78c64fe..c6c31791f 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -253,15 +253,17 @@ End contractive.
Ltac f_contractive :=
match goal with
- | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> _) f)
- | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> _) f)
- | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> _) f)
+ | |- ?f _ ≡{_}≡ ?f _ => simple apply (_ : Proper (dist_later _ ==> dist _) f)
+ | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (dist_later _ ==> _ ==> dist _) f)
+ | |- ?f _ _ ≡{_}≡ ?f _ _ => simple apply (_ : Proper (_ ==> dist_later _ ==> dist _) f)
end;
try match goal with
| |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end;
- try simple apply reflexivity.
+ (* Only try reflexivity if the terms are syntactically equal. This avoids
+ very expensive failing unification. *)
+ try match goal with |- _ ?x ?x => simple apply reflexivity end.
Ltac solve_contractive :=
solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
--
GitLab