Tweak sealing stuff.

* Use sig instead of sigT: the proof is a Prop after all
* Tweak implicit arguments
* Shorten proof of sigma

heap_lang/heap.v

@@ -25,11 +25,10 @@ matching it against other forms of ownership. *)
 Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
   auth_own heap_name {[ l := Excl v ]}.
 (* Perform sealing *)
-Definition heap_mapsto_aux : { x : _ & x = @heap_mapsto_def }.
-  exact (existT _ Logic.eq_refl). Qed.
-Definition heap_mapsto := projT1 heap_mapsto_aux.
-Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := projT2 heap_mapsto_aux.
-Arguments heap_mapsto {_ _} _ _.
+Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
+Definition heap_mapsto {Σ h} := proj1_sig heap_mapsto_aux Σ h.
+Definition heap_mapsto_eq :
+  @heap_mapsto = @heap_mapsto_def := proj2_sig heap_mapsto_aux.
 
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).

program_logic/auth.v

@@ -16,11 +16,9 @@ Proof. split; try apply _. apply: inGF_inG. Qed.
 Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   own γ (◯ a).
 (* Perform sealing *)
-Definition auth_own_aux : { x : _ & x = @auth_own_def }.
-  exact (existT _ Logic.eq_refl). Qed.
-Definition auth_own := projT1 auth_own_aux.
-Definition auth_own_eq : @auth_own = @auth_own_def := projT2 auth_own_aux.
-Arguments auth_own {_ _ _ _ _} _ _.
+Definition auth_own_aux : { x | x = @auth_own_def }. by eexists. Qed.
+Definition auth_own {Λ Σ A Ae a} := proj1_sig auth_own_aux Λ Σ A Ae a.
+Definition auth_own_eq : @auth_own = @auth_own_def := proj2_sig auth_own_aux.
 
 Definition auth_inv `{authG Λ Σ A}
     (γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=

program_logic/saved_prop.v

@@ -12,11 +12,11 @@ Definition saved_prop_own_def `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).
 (* Perform sealing *)
-Definition saved_prop_own_aux : { x : _ & x = @saved_prop_own_def }.
-  exact (existT _ Logic.eq_refl). Qed.
-Definition saved_prop_own := projT1 saved_prop_own_aux.
-Definition saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def := projT2 saved_prop_own_aux.
-Arguments saved_prop_own {_ _ _} _ _.
+Definition saved_prop_own_aux : { x | x = @saved_prop_own_def }. by eexists. Qed.
+Definition saved_prop_own {Λ Σ s} := proj1_sig saved_prop_own_aux Λ Σ s.
+Definition saved_prop_own_eq :
+  @saved_prop_own = @saved_prop_own_def := proj2_sig saved_prop_own_aux.
+
 Instance: Params (@saved_prop_own) 4.
 
 Section saved_prop.

program_logic/sts.v

@@ -14,30 +14,26 @@ Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
 Proof. split; try apply _. apply: inGF_inG. Qed.
 
 Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
-           (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
+    (S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
   own γ (sts_frag S T).
 (* Perform sealing. *)
-Definition sts_ownS_aux : { x : _ & x = @sts_ownS_def }.
-  exact (existT _ Logic.eq_refl). Qed.
-Definition sts_ownS := projT1 sts_ownS_aux.
-Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := projT2 sts_ownS_aux.
-Arguments sts_ownS {_ _ _ _} _ _ _.
+Definition sts_ownS_aux : { x | x = @sts_ownS_def }. by eexists. Qed.
+Definition sts_ownS {Λ Σ sts i} := proj1_sig sts_ownS_aux Λ Σ sts i.
+Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := proj2_sig sts_ownS_aux.
 
 Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
-           (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
+    (s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
   own γ (sts_frag_up s T).
 (* Perform sealing. *)
-Definition sts_own_aux : { x : _ & x = @sts_own_def }.
-  exact (existT _ Logic.eq_refl). Qed.
-Definition sts_own := projT1 sts_own_aux.
-Definition sts_own_eq : @sts_own = @sts_own_def := projT2 sts_own_aux.
-Arguments sts_own {_ _ _ _} _ _ _.
+Definition sts_own_aux : { x | x = @sts_own_def }. by eexists. Qed.
+Definition sts_own {Λ Σ sts i} := proj1_sig sts_own_aux Λ Σ sts i.
+Definition sts_own_eq : @sts_own = @sts_own_def := proj2_sig sts_own_aux.
 
 Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
-           (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   (∃ s, own γ (sts_auth s ∅) ★ φ s)%I.
 Definition sts_ctx `{i : stsG Λ Σ sts} (γ : gname)
-           (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (N : namespace) (φ: sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
   inv N (sts_inv γ φ).
 
 Instance: Params (@sts_inv) 5.