From fb1712dd9da4d05ca2c919748633801934369d0d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 26 Dec 2016 10:02:59 +0100
Subject: [PATCH] Make f_contractive more robust.
---
theories/algebra/ofe.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 6804c1720..c0cf52f36 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -179,7 +179,8 @@ Ltac f_contractive :=
| |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
end;
try match goal with
- | |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x ≡{n}≡ y)]
+ | |- @dist_later ?A ?n ?x ?y =>
+ destruct n as [|n]; [done|change (@dist A _ n x y)]
end;
try reflexivity.
--
GitLab