From 1742020952b3c3d0dc2d99921fb2c70c2af166a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Nov 2017 00:22:32 +0100
Subject: [PATCH] Remove some unused eauto arguments.

---
 theories/heap_lang/tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 37af82a7d..5602dd515 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -114,7 +114,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
 Proof.
   revert X.
-  induction e; naive_solver eauto using is_closed_of_val, is_closed_to_val, is_closed_weaken_nil.
+  induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
 Qed.
 
 (* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
@@ -172,7 +172,7 @@ Lemma to_expr_subst x er e :
   to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
 Proof.
   induction e; simpl; repeat case_decide;
-    f_equal; eauto using subst_is_closed_nil, is_closed_of_val, is_closed_to_val, eq_sym.
+    f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
 Qed.
 
 Definition atomic (e : expr) :=
-- 
GitLab