diff --git a/theories/decidable.v b/theories/decidable.v
index aecd65d0e3296783e38e81284479d21630a83c95..81c18b8fd7cc292e8670c09c064563920c2d4dd1 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -11,7 +11,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
-Proof. destruct b. by left. right. intros []. Qed.
+Proof. destruct b. left; constructor. right. intros []. Qed.
 Instance: Inj (=) (↔) Is_true.
 Proof. intros [] []; simpl; intuition. Qed.
 
@@ -24,17 +24,17 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x
   (x : A) (y : B) : Decision (R x y) := dec x y.
 Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y)}
   (x : A) (y : B) : decide_rel R x y = decide (R x y).
-Proof. done. Qed.
+Proof. reflexivity. Qed.
 
 Lemma decide_True {A} `{Decision P} (x y : A) :
   P → (if decide P then x else y) = x.
-Proof. by destruct (decide P). Qed.
+Proof. destruct (decide P); tauto. Qed.
 Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
-Proof. by destruct (decide P). Qed.
+Proof. destruct (decide P); tauto. Qed.
 Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
-Proof. intros [??]. destruct (decide P), (decide Q); intuition. Qed.
+Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
 components is double negated, it will try to remove the double negation. *)
@@ -95,7 +95,7 @@ Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
 
 Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
-Proof. unfold bool_decide. destruct dec. by left. by right. Qed.
+Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
 
 Tactic Notation "case_bool_decide" "as" ident (Hd) :=
   match goal with
@@ -108,15 +108,15 @@ Tactic Notation "case_bool_decide" :=
   let H := fresh in case_bool_decide as H.
 
 Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P.
-Proof. unfold bool_decide. by destruct dec. Qed.
+Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
 Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
-Proof. by rewrite bool_decide_spec. Qed.
+Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
-Proof. by rewrite bool_decide_spec. Qed.
+Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
-Proof. by case_bool_decide. Qed.
+Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
-Proof. by case_bool_decide. Qed.
+Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
 Proof. repeat case_bool_decide; tauto. Qed.
@@ -138,7 +138,7 @@ Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
 Proof. apply (sig_eq_pi _). Qed.
 Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
-Proof. by apply dsig_eq. Qed.
+Proof. apply dsig_eq; reflexivity. Qed.
 
 (** * Instances of Decision *)
 (** Instances of [Decision] for operators of propositional logic. *)
@@ -184,7 +184,7 @@ Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
 
 Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
-Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
+Proof. refine (cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined.
 
 (** Some laws for decidable propositions *)
 Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
diff --git a/theories/list.v b/theories/list.v
index 5042b8e842e602d33bede86426440c464f3b754b..7dcf11c6cc76f21940c5e047746ba274f7398c73 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3,7 +3,7 @@
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
 From Coq Require Export Permutation.
-From stdpp Require Export numbers base decidable option.
+From stdpp Require Export numbers base option.
 
 Arguments length {_} _.
 Arguments cons {_} _ _.
diff --git a/theories/listset.v b/theories/listset.v
index 09eb5e3a318f04aa8ed9addc90600f6a5ff3b6e9..efca035d75a65e8522fbe44687f3ecedac3d7db5 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
-From stdpp Require Export base decidable collections list.
+From stdpp Require Export collections list.
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 6140a10320593c4637dd90a391108bd117697dfb..a67fa04b87739f61ee3572837a203f6c1f0c8ef1 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -3,7 +3,7 @@
 (** This file implements finite as unordered lists without duplicates.
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
-From stdpp Require Export base decidable collections list.
+From stdpp Require Export collections list.
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/theories/option.v b/theories/option.v
index 66d375d121c325526a76aafc718470873d2d250c..f66ee25902a3f1b041af2557b1309cc3147053fd 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
-From stdpp Require Export base tactics decidable.
+From stdpp Require Export tactics.
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/theories/orders.v b/theories/orders.v
index 743f1afb9fa4f38994e6606ab5ab19677ec31f63..40a9f1045ca58c3f92b9e67400c8fcfa16ab36ba 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -3,7 +3,7 @@
 (** This file collects common properties of pre-orders and semi lattices. This
 theory will mainly be used for the theory on collections and finite maps. *)
 From Coq Require Export Sorted.
-From stdpp Require Export base decidable tactics list.
+From stdpp Require Export tactics list.
 
 (** * Arbitrary pre-, parial and total orders *)
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
diff --git a/theories/prelude.v b/theories/prelude.v
index 34c65d5a15868eae9d6d3f6c8d10be0a4a086f31..1d4b126826c43a3f9604445013b8ab315b7e1686 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -3,7 +3,6 @@
 From stdpp Require Export
   base
   tactics
-  decidable
   orders
   option
   vector
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index afb9297a926119002f2c9b94da543f1628be5604..8b3769dcddb9745fdf0927a5cfa4de798364bcf8 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -2,20 +2,20 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 From Coq Require Import Eqdep_dec.
-From stdpp Require Export tactics.
+From stdpp Require Export base.
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
 Instance: ProofIrrel True.
-Proof. by intros [] []. Qed.
+Proof. intros [] []; reflexivity. Qed.
 Instance: ProofIrrel False.
-Proof. by intros []. Qed.
+Proof. intros []. Qed.
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
-Proof. intros ?? [??] [??]. by f_equal. Qed.
+Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
 Instance prod_pi (A B : Type) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
-Proof. intros ?? [??] [??]. by f_equal. Qed.
+Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
 Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) :
   ProofIrrel (x = y).
 Proof.
@@ -27,10 +27,10 @@ Proof. destruct b; simpl; apply _. Qed.
 Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x y : sig P) : x = y ↔ `x = `y.
 Proof.
-  split; [by intros <- |].
+  split; [intros <-; reflexivity|].
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x : sig P) p : `x ↾ p = x.
-Proof. by apply (sig_eq_pi _). Qed.
+Proof. apply (sig_eq_pi _); reflexivity. Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index 45d975a5e1c611e5442d14f27450aa2b18fe4935..6ba160cbb042678a98b8a015af3404693003c909 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -4,7 +4,7 @@
 the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Psatz.
-From stdpp Require Export base.
+From stdpp Require Export decidable.
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
@@ -430,6 +430,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : _ ∧ _ |- _ => destruct H
   | H : ∃ _, _  |- _ => destruct H
   | H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
+  | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
+  | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
   (**i solve the goal *)
@@ -441,6 +443,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
     | reflexivity ]
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
+  | |- Is_true (bool_decide _) => apply (bool_decide_pack _)
+  | |- Is_true (_ && _) => apply andb_True; split
   | H : _ ∨ _ |- _ => destruct H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]