From 31a1a1c361b8d835d6dbca981903e01cb59ec3b6 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Fri, 13 Mar 2020 01:06:43 +0100 Subject: [PATCH] examples.v: fix import order --- theories/Dot/examples/examples.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/theories/Dot/examples/examples.v b/theories/Dot/examples/examples.v index 1a1a0c941..0ad070c7b 100644 --- a/theories/Dot/examples/examples.v +++ b/theories/Dot/examples/examples.v @@ -1,6 +1,9 @@ From iris.proofmode Require Import tactics. From D.pure_program_logic Require Import lifting adequacy. From iris.program_logic Require Import ectxi_language. +From D.Dot Require Import dlang_inst. + +Import dlang_adequacy. From D Require Import swap_later_impl. From D.Dot Require Import scalaLib hoas exampleInfra typingExInfra. @@ -9,7 +12,6 @@ From D.Dot Require Import unary_lr lr_lemmas lr_lemmasTSel lr_lemmasNoBinding lr_lemmasDefs lr_lemmasPrim. From D.Dot Require Import typeExtractionSem. From D.Dot Require Import skeleton fundamental. -Import dlang_adequacy. Set Suggest Proof Using. Set Default Proof Using "Type". @@ -290,7 +292,7 @@ Section div_example. iPoseProof (sToIpos with "Hs") as "Hs2/=". iPoseProof (dm_to_type_agree vnil (ρ 0) with "Hs1 Hs2") as "{Hs Hs1 Hs2} Heq". wp_bind (BinRCtx _ _); rewrite -wp_pure_step_later // -wp_value/=/lang.of_val. - iNext. iRewrite "Heq" in "Harg"; iClear "Heq". + iNext. iRewrite "Heq" in "Harg". iClear "Heq". by iApply wp_div_spec. Qed. End div_example.