examples.v: fix import order

Blaisorblade · Mar 23, 2020 · 31a1a1c · 31a1a1c
1 parent 914b507
commit 31a1a1c
Showing 1 changed file with 4 additions and 2 deletions.
diff --git 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.