diff --git a/msl/subtypes_sl.v b/msl/subtypes_sl.v
index e7c463880..876e31f23 100644
--- a/msl/subtypes_sl.v
+++ b/msl/subtypes_sl.v
@@ -127,7 +127,6 @@ Qed.
 Lemma pred_eq_e2 {A} `{agA : ageable A} {EO: Ext_ord A}: forall (P Q: pred A)  w,
      ((P <=> Q) w -> (Q >=> P) w).
 Proof.
-Proof.
 intros.
 intros w' ? w'' ? ?.
 eapply H; eauto.
diff --git a/veric/NullExtension.v b/veric/NullExtension.v
index 4667c2254..03fa7e1f4 100644
--- a/veric/NullExtension.v
+++ b/veric/NullExtension.v
@@ -19,8 +19,8 @@ Definition juicyspec : external_specification juicy_mem external_function unit
      (fun rv m z => True).
 
 Definition Espec : OracleKind.
- refine (Build_OracleKind unit (Build_juicy_ext_spec _ juicyspec _ _ _ _ _ _)).
 Proof.
+refine (Build_OracleKind unit (Build_juicy_ext_spec _ juicyspec _ _ _ _ _ _)).
 simpl; intros; contradiction.
 simpl; intros; contradiction.
 simpl; intros; intros ? ? ? ?; contradiction.
@@ -101,4 +101,4 @@ Lemma module_sequential_safety : (*TODO*)
        forall n, safeN_(genv_symb := @semax.genv_symb_injective _ _)(Hrel := fun _ => juicy_extspec.Hrel)
             sem  (upd_exit (@OK_spec spec) x (semax.genv_symb_injective ge)) 
            ge n ora q m.
-Abort.
\ No newline at end of file
+Abort.
diff --git a/veric/initialize.v b/veric/initialize.v
index f71d5e31c..9d61ce707 100644
--- a/veric/initialize.v
+++ b/veric/initialize.v
@@ -16,9 +16,9 @@ Import compcert.lib.Maps.
 Import Clight.
 
 Definition only_blocks {S: block -> Prop} (S_dec: forall b, {S b}+{~S b}) (w: rmap) : rmap.
+Proof.
  refine (proj1_sig (make_rmap (fun loc => if S_dec (fst loc) then w @ loc else core (w @ loc))
                               _ (level w) _ (ghost_of_approx w))).
-Proof.
   hnf; auto.
  extensionality loc;  unfold compose.
  if_tac; try apply resource_at_approx.
diff --git a/veric/juicy_extspec.v b/veric/juicy_extspec.v
index 30a01fbad..8e0bf7869 100644
--- a/veric/juicy_extspec.v
+++ b/veric/juicy_extspec.v
@@ -45,8 +45,8 @@ Definition void_spec T : external_specification juicy_mem external_function T :=
       (fun rv m z => False).
 
 Definition ok_void_spec (T : Type) : OracleKind.
- refine (Build_OracleKind T (Build_juicy_ext_spec _ (void_spec T) _ _ _ _ _ _)).
 Proof.
+  refine (Build_OracleKind T (Build_juicy_ext_spec _ (void_spec T) _ _ _ _ _ _)).
   simpl; intros; contradiction.
   simpl; intros; contradiction.
   simpl; intros; contradiction.
diff --git a/veric/juicy_mem.v b/veric/juicy_mem.v
index a879b6d26..676d6f585 100644
--- a/veric/juicy_mem.v
+++ b/veric/juicy_mem.v
@@ -961,7 +961,8 @@ Qed.
 (* FIXME
    Build an rmap that's identical to phi except where m has allocated. *)
 Definition inflate_alloc: rmap.
- refine (proj1_sig (remake_rmap (fun loc =>
+Proof.
+refine (proj1_sig (remake_rmap (fun loc =>
    fmap_option (res_option (phi @ loc))
 
   (* phi = NO *)
@@ -975,7 +976,6 @@ Definition inflate_alloc: rmap.
 
   (* phi = YES *)
   (fun _ => phi @ loc)) (ghost_of phi) (level phi) _ (ghost_of_approx phi))).
-Proof.
 hnf; auto.
 intro.
 case_eq (phi @ l); simpl; intros; auto.
@@ -999,14 +999,15 @@ auto.
 Qed.
 
 (* Build an [rmap] that's identical to [phi] except where [m] has stored. *)
-Definition inflate_store: rmap. refine (
+Definition inflate_store: rmap.
+Proof.
+refine (
 proj1_sig (make_rmap (fun loc =>
   match phi @ loc with
     | YES sh rsh (VAL _) _ => YES sh rsh (VAL (contents_at m loc)) NoneP
     | YES _ _ _ _ => resource_fmap (approx (level phi)) (approx (level phi)) (phi @ loc)
     | _ => phi @ loc
   end) (ghost_of phi) (level phi) _ (ghost_of_approx phi))).
-Proof.
 hnf; auto.
 
 unfold compose.
@@ -1521,12 +1522,13 @@ Variables (jm :juicy_mem) (m': mem)
           (PERM: forall ofs, lo <= ofs < hi ->
                       perm_of_res (m_phi jm @ (b,ofs)) = Some Freeable).
 
-Definition inflate_free: rmap. refine (
+Definition inflate_free: rmap.
+Proof.
+refine (
 proj1_sig (make_rmap (fun loc =>
   if adr_range_dec (b,lo) (hi-lo) loc then NO Share.bot bot_unreadable else m_phi jm @ loc)
     (ghost_of (m_phi jm))
      (level (m_phi jm)) _ (ghost_of_approx (m_phi jm)))).
-Proof.
 unfold compose.
 extensionality l.
 destruct l as (b', ofs').
diff --git a/veric/splice.v b/veric/splice.v
index 4d631e015..c84310f81 100644
--- a/veric/splice.v
+++ b/veric/splice.v
@@ -335,8 +335,8 @@ Proof.
 Qed.
 
 Lemma readable_share_unrel_Rsh: forall sh, readable_share sh <-> nonunit (Share.unrel Share.Rsh sh).
-unfold readable_share in *.
 Proof.
+unfold readable_share in *.
 intros.
 unfold nonempty_share.
 transitivity (nonidentity (Share.unrel Share.Rsh sh)).