From 61dd9360151e09dfd04b552147d545498417eb5f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 26 Oct 2021 21:59:43 +0200
Subject: [PATCH] well_founded.v: stop requiring tactics

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

diff --git a/theories/well_founded.v b/theories/well_founded.v
index 8eeac9e3..4a4a7003 100644
--- a/theories/well_founded.v
+++ b/theories/well_founded.v
@@ -1,10 +1,10 @@
 (** * Theorems on well founded relations *)
-From stdpp Require Import base tactics.
+From stdpp Require Import base.
 From stdpp Require Import options.
 
 Lemma Acc_impl {A} (R1 R2 : relation A) x :
   Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
-Proof. induction 1; constructor; naive_solver. Qed.
+Proof. induction 1; constructor; auto. Qed.
 
 Notation wf := well_founded.
 
-- 
GitLab