From 466f1be9324c5dd478e47af69c03b86804463ce3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:24:38 +0100
Subject: [PATCH] Set Obligation Tactic := idtac globally.

---
 channel/heap_lang.v       |  1 -
 modures/cofe.v            |  1 -
 modures/fin_maps.v        |  1 -
 prelude/base.v            |  1 +
 prelude/countable.v       |  1 -
 prelude/fin_collections.v |  8 ++++----
 prelude/finite.v          |  1 -
 prelude/hashset.v         |  8 ++++----
 prelude/numbers.v         | 20 ++++++++------------
 9 files changed, 17 insertions(+), 25 deletions(-)

diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index 2e58ca3bb..b1bc26f03 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -405,7 +405,6 @@ End Tests.
 (** Instantiate the Iris language interface. This closes reduction under evaluation contexts.
     We could potentially make this a generic construction. *)
 Section Language.
-  Local Obligation Tactic := idtac.
 
   Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
     exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.
diff --git a/modures/cofe.v b/modures/cofe.v
index adfaa867a..1f249d37c 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -1,5 +1,4 @@
 Require Export prelude.prelude.
-Obligation Tactic := idtac.
 
 (** Unbundeled version *)
 Class Dist A := dist : nat → relation A.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 76b2abe46..65267bb0f 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -1,6 +1,5 @@
 Require Export modures.cmra prelude.gmap.
 Require Import modures.option.
-Local Obligation Tactic := idtac.
 
 Section map.
 Context `{Countable K}.
diff --git a/prelude/base.v b/prelude/base.v
index a81acf17a..f42df42af 100644
--- a/prelude/base.v
+++ b/prelude/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/prelude/countable.v b/prelude/countable.v
index 71fe2f0d4..ab860ddf6 100644
--- a/prelude/countable.v
+++ b/prelude/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/prelude/fin_collections.v b/prelude/fin_collections.v
index 0dd6333eb..60e971e5f 100644
--- a/prelude/fin_collections.v
+++ b/prelude/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/prelude/finite.v b/prelude/finite.v
index fed9dd3f7..76006bf3a 100644
--- a/prelude/finite.v
+++ b/prelude/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/prelude/hashset.v b/prelude/hashset.v
index d01bf1b8c..efddcf1b3 100644
--- a/prelude/hashset.v
+++ b/prelude/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/prelude/numbers.v b/prelude/numbers.v
index 2a2c038b1..65b9621e9 100644
--- a/prelude/numbers.v
+++ b/prelude/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.
-- 
GitLab