diff --git a/theories/base.v b/theories/base.v
index a81acf17ae3117104dc27960658b686daa4b92f9..f42df42affd16dcf8734e3f223fec3b0b295509e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -8,6 +8,7 @@ Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
+Obligation Tactic := idtac.
 
 (** * General *)
 (** Zipping lists. *)
diff --git a/theories/countable.v b/theories/countable.v
index 71fe2f0d472f60fc7da4e41424b42f6842f05c33..ab860ddf677228e3cf49060c021ffab5fa1e61db 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,7 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 Require Export prelude.list.
-Local Obligation Tactic := idtac.
 Local Open Scope positive.
 
 Class Countable A `{∀ x y : A, Decision (x = y)} := {
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 0dd6333eb16d2407b67e6340149b562659ffb401..60e971e5f01f266dabae251cb5a2e218f84bd2b4 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -93,15 +93,15 @@ Proof.
 Defined.
 Global Program Instance collection_subseteq_dec_slow (X Y : C) :
     Decision (X ⊆ Y) | 100 :=
-  match decide_rel (=) (size (X ∖ Y)) 0 with
-  | left E1 => left _ | right E1 => right _
+  match decide_rel (=) (size (X ∖ Y)) 0 return _ with
+  | left _ => left _ | right _ => right _
   end.
 Next Obligation.
-  intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
+  intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)).
   apply (size_empty_inv _ E1). by rewrite elem_of_difference.
 Qed.
 Next Obligation.
-  intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
+  intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x.
   rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
 Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
diff --git a/theories/finite.v b/theories/finite.v
index fed9dd3f795fd9e68de56e561956edf16c007731..76006bf3a8d8596ce3256f95c0e0271f7e8e5cad 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,7 +1,6 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 Require Export prelude.countable prelude.list.
-Obligation Tactic := idtac.
 
 Class Finite A `{∀ x y : A, Decision (x = y)} := {
   enum : list A;
diff --git a/theories/hashset.v b/theories/hashset.v
index d01bf1b8c18709dbb695bfe77c070f11d6ef1c9b..efddcf1b36e9005f2886a49116fe0d39e945c50d 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -25,14 +25,14 @@ Next Obligation. by intros n X; simpl_map. Qed.
 Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
   Hashset {[ hash x ↦ [x] ]} _.
 Next Obligation.
-  intros n l. rewrite lookup_singleton_Some. intros [<- <-].
+  intros x n l [<- <-]%lookup_singleton_Some.
   rewrite Forall_singleton; auto using NoDup_singleton.
 Qed.
 Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. 
 Next Obligation.
-  intros n l'. rewrite lookup_union_with_Some.
+  intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
   intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_equality'; auto.
   split; [apply Forall_list_union|apply NoDup_list_union];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
@@ -42,7 +42,7 @@ Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
   Hashset (intersection_with (λ l k,
     let l' := list_intersection l k in guard (l' ≠ []); Some l') m1 m2) _.
 Next Obligation.
-  intros n l'. rewrite lookup_intersection_with_Some.
+  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
   intros (?&?&?&?&?); simplify_option_equality.
   split; [apply Forall_list_intersection|apply NoDup_list_intersection];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
@@ -52,7 +52,7 @@ Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
   Hashset (difference_with (λ l k,
     let l' := list_difference l k in guard (l' ≠ []); Some l') m1 m2) _.
 Next Obligation.
-  intros n l'. rewrite lookup_difference_with_Some.
+  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
   intros [[??]|(?&?&?&?&?)]; simplify_option_equality; auto.
   split; [apply Forall_list_difference|apply NoDup_list_difference];
     first [by eapply Hm1; eauto | by eapply Hm2; eauto].
diff --git a/theories/numbers.v b/theories/numbers.v
index 2a2c038b12d1e2af2713b5f7faa69732974a9540..65b9621e9377f9720ca2ba31bcf158a03ac2c302 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -189,17 +189,11 @@ Proof. by injection 1. Qed.
 
 Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec.
 Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N :=
-  match Ncompare x y with
-  | Gt => right _
-  | _ => left _
-  end.
-Next Obligation. congruence. Qed.
+  match Ncompare x y with Gt => right _ | _ => left _ end.
+Solve Obligations with naive_solver.
 Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
-  match Ncompare x y with
-  | Lt => left _
-  | _ => right _
-  end.
-Next Obligation. congruence. Qed.
+  match Ncompare x y with Lt => left _ | _ => right _ end.
+Solve Obligations with naive_solver.
 Instance N_inhabited: Inhabited N := populate 1%N.
 Instance: PartialOrder (≤)%N.
 Proof.
@@ -340,10 +334,12 @@ Arguments Qred _ : simpl never.
 Instance Qc_eq_dec: ∀ x y : Qc, Decision (x = y) := Qc_eq_dec.
 Program Instance Qc_le_dec (x y : Qc) : Decision (x ≤ y) :=
   if Qclt_le_dec y x then right _ else left _.
-Next Obligation. by apply Qclt_not_le. Qed.
+Next Obligation. intros x y; apply Qclt_not_le. Qed.
+Next Obligation. done. Qed.
 Program Instance Qc_lt_dec (x y : Qc) : Decision (x < y) :=
   if Qclt_le_dec x y then left _ else right _.
-Next Obligation. by apply Qcle_not_lt. Qed.
+Solve Obligations with done.
+Next Obligation. intros x y; apply Qcle_not_lt. Qed.
 
 Instance: PartialOrder (≤).
 Proof.