From 2232cb4b1009c29b95c6b00cc45efcda0a466611 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Mar 2018 17:39:09 +0100
Subject: [PATCH] remove unused admitted lemma

---
 theories/tactics_vProp.v | 21 ---------------------
 1 file changed, 21 deletions(-)

diff --git a/theories/tactics_vProp.v b/theories/tactics_vProp.v
index 0169eb4d..6e085ac5 100644
--- a/theories/tactics_vProp.v
+++ b/theories/tactics_vProp.v
@@ -5,27 +5,6 @@ From igps Require tactics.
 Import base.
 
 
-Lemma atomic_correct e V : tactics.W.atomic0 e →
-                           Atomic (Λ:=ra_lang) WeaklyAtomic (tactics.W.to_expr' e,V).
-Proof.
-(*   intros He. apply ectx_language_atomic; last first. *)
-(*   - apply ectxi_language_sub_redexes_are_values => /= Ki [e' V'] Hfill. *)
-(*     (destruct e=> //); destruct Ki; repeat (simplify_eq; case_match=>//); *)
-(*     rewrite /= /ra_lang.fill_item /fill_item /= in Hfill; *)
-(*     inversion Hfill; subst; *)
-(*     try rewrite decide_left; eauto. *)
-(*     move: He. rewrite [atomic _]/=. repeat (case_match) => // _. *)
-(*     apply to_val_is_Some'. econstructor.  *)
-(*     naive_solver eauto using to_val_is_Some'. *)
-(*   - intros σ e' σ' ef Hstep; simpl in *. *)
-(*     apply language.val_irreducible; revert Hstep. *)
-(*     destruct e', e => //=. simplify_eq. inversion 1. simplify_eq. *)
-(*     destruct e=> //=; repeat (simplify_eq/=; case_match=>//); *)
-(*       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto. *)
-(*     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto. *)
-(* Qed. *)
-Admitted.
-
 Ltac solve_closed :=
   match goal with
   | |- Closed ?X ?e =>
-- 
GitLab