From 8513ff5ea95fd7e40647b2eec12dc4815d80875e Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 19 Jan 2016 10:08:19 +0100
Subject: [PATCH] make parameter.v compile again
---
iris/parameter.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/iris/parameter.v b/iris/parameter.v
index 8c6c1e35f..66a71493c 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -18,7 +18,7 @@ Record iParam := IParam {
icmra_map (g ◎ f) x ≡ icmra_map g (icmra_map f x);
icmra_map_mono {A B} (f : A -n> B) : CMRAMonotone (icmra_map f)
}.
-Arguments IParam {_ _ _} _ _ {_ _} _ {_ _ _ _}.
+Arguments IParam {_ _ _} ilanguage icmra {_ _ _} _ {_ _ _ _}.
Existing Instances ilanguage.
Existing Instances icmra_empty icmra_empty_spec icmra_empty_timeless.
Existing Instances icmra_map_ne icmra_map_mono.
@@ -32,7 +32,7 @@ Qed.
Definition IParamConst {iexpr ival istate : Type}
(ilanguage : Language iexpr ival istate)
(icmra : cmraT) {icmra_empty : Empty icmra}
- {icmra_empty_spec : RAIdentity icmra}:
+ {icmra_empty_spec : RAIdentity icmra} {icmra_empty_timeless: Timeless (∅ : icmra)}:
iParam.
eapply (IParam ilanguage (fun _ => icmra) (fun _ _ _ => cid)).
Unshelve.
--
GitLab