From e8ce5b3835391c82343462b7520e1fad969e0d8f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Mar 2016 17:01:01 +0100
Subject: [PATCH] test for 'crazy higher order'

---
 program_logic/tests.v | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/program_logic/tests.v b/program_logic/tests.v
index 9d81b5333..ab4240209 100644
--- a/program_logic/tests.v
+++ b/program_logic/tests.v
@@ -1,7 +1,21 @@
 (** This file tests a bunch of things. *)
-From program_logic Require Import model.
+From program_logic Require Import model saved_prop.
 
 Module ModelTest. (* Make sure we got the notations right. *)
   Definition iResTest {Λ : language} {Σ : rFunctor}
     (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
 End ModelTest.
+
+Module SavedPropTest.
+  (* Test if we can really go "crazy higher order" *)
+  Section sec.
+    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF idCF idCF) ].
+    Context {Λ : language}.
+    Notation iProp := (iPropG Λ Σ).
+
+    Local Instance : savedPropG Λ Σ (cofe_morCF idCF idCF) := _.
+
+    Definition own_pred γ (φ : laterC iProp -n> laterC iProp) : iProp :=
+      saved_prop_own γ φ.
+  End sec.
+End SavedPropTest.
-- 
GitLab