Commit 3458ec75 authored by Tej Chajed's avatar Tej Chajed

Explicitly use core hint database

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).
parent be4eb648
......@@ -166,8 +166,8 @@ Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
(at level 70, only parsing, no associativity) : stdpp_scope.
Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ _) => discriminate.
Hint Extern 0 (_ = _) => reflexivity : core.
Hint Extern 100 (_ _) => discriminate : core.
Instance: A, PreOrder (=@{A}).
Proof. split; repeat intro; congruence. Qed.
......@@ -234,8 +234,8 @@ Instance: Params (@equiv) 2.
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ _) => symmetry; assumption.
Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core.
(** * Type classes *)
......@@ -406,8 +406,8 @@ Notation "(↔)" := iff (only parsing) : stdpp_scope.
Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
Notation "(↔ B )" := (λ A, A B) (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ _) => symmetry; assumption.
Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core.
Lemma or_l P Q : ¬Q P Q P.
Proof. tauto. Qed.
......@@ -539,9 +539,9 @@ Notation zip := (zip_with pair).
(** ** Booleans *)
(** The following coercion allows us to use Booleans as propositions. *)
Coercion Is_true : bool >-> Sortclass.
Hint Unfold Is_true.
Hint Immediate Is_true_eq_left.
Hint Resolve orb_prop_intro andb_prop_intro.
Hint Unfold Is_true : core.
Hint Immediate Is_true_eq_left : core.
Hint Resolve orb_prop_intro andb_prop_intro : core.
Notation "(&&)" := andb (only parsing).
Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
......@@ -826,9 +826,9 @@ Infix "⊆2*" := (Forall2 (λ p q, p.2 ⊆ q.2)) (at level 70) : stdpp_scope.
Infix "⊆1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : stdpp_scope.
Infix "⊆2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ * _) => reflexivity.
Hint Extern 0 (_ ** _) => reflexivity.
Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ * _) => reflexivity : core.
Hint Extern 0 (_ ** _) => reflexivity : core.
Infix "⊂" := (strict ()) (at level 70) : stdpp_scope.
Notation "(⊂)" := (strict ()) (only parsing) : stdpp_scope.
......@@ -886,8 +886,8 @@ Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : stdpp_scope.
Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : stdpp_scope.
Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : stdpp_scope.
Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : stdpp_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ##* _) => symmetry; eassumption.
Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
Class DisjointE E A := disjointE : E A A Prop.
Hint Mode DisjointE - ! : typeclass_instances.
......@@ -904,7 +904,7 @@ Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ
Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
(Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
(at level 70, format "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys") : stdpp_scope.
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
Class DisjointList A := disjoint_list : list A Prop.
Hint Mode DisjointList ! : typeclass_instances.
......@@ -1212,7 +1212,7 @@ Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation ().
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ _) => reflexivity : core.
Class Meet A := meet: A A A.
Hint Mode Meet ! : typeclass_instances.
......
......@@ -36,7 +36,7 @@ Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r) coPset_wf r.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate coPNode_wf_l coPNode_wf_r.
Local Hint Immediate coPNode_wf_l coPNode_wf_r : core.
Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
match b, l, r with
......@@ -47,7 +47,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
Arguments coPNode' : simpl never.
Lemma coPNode_wf b l r : coPset_wf l coPset_wf r coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
Hint Resolve coPNode_wf.
Hint Resolve coPNode_wf : core.
Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
match t, p with
......@@ -207,7 +207,7 @@ Defined.
(** * Top *)
Lemma coPset_top_subseteq (X : coPset) : X .
Proof. done. Qed.
Hint Resolve coPset_top_subseteq.
Hint Resolve coPset_top_subseteq : core.
(** * Finite sets *)
Fixpoint coPset_finite (t : coPset_raw) : bool :=
......
......@@ -107,7 +107,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack.
Hint Resolve bool_decide_pack : core.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. case_bool_decide; tauto. Qed.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false.
......
......@@ -97,7 +97,7 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ## m) (only parsing) : stdpp_scope.
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
......
......@@ -261,7 +261,7 @@ Defined.
Lemma gmultiset_subset_subseteq X Y : X Y X Y.
Proof. apply strict_include. Qed.
Hint Resolve gmultiset_subset_subseteq.
Hint Resolve gmultiset_subset_subseteq : core.
Lemma gmultiset_empty_subseteq X : X.
Proof. intros x. rewrite multiplicity_empty. lia. Qed.
......
......@@ -246,8 +246,8 @@ Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2, k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
Hint Extern 0 (_ `prefix_of` _) => reflexivity : core.
Hint Extern 0 (_ `suffix_of` _) => reflexivity : core.
Section prefix_suffix_ops.
Context `{EqDecision A}.
......@@ -276,7 +276,7 @@ Inductive sublist {A} : relation (list A) :=
| sublist_skip x l1 l2 : sublist l1 l2 sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 sublist l1 (x :: l2).
Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
Hint Extern 0 (_ `sublist_of` _) => reflexivity.
Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
from [l1] while possiblity changing the order. *)
......@@ -287,7 +287,7 @@ Inductive submseteq {A} : relation (list A) :=
| submseteq_cons x l1 l2 : submseteq l1 l2 submseteq l1 (x :: l2)
| submseteq_trans l1 l2 l3 : submseteq l1 l2 submseteq l2 l3 submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
Hint Extern 0 (_ + _) => reflexivity.
Hint Extern 0 (_ + _) => reflexivity : core.
(** Removes [x] from the list [l]. The function returns a [Some] when the
+removal succeeds and [None] when [x] is not in [l]. *)
......@@ -2760,7 +2760,7 @@ End Forall2_proper.
Section Forall3.
Context {A B C} (P : A B C Prop).
Hint Extern 0 (Forall3 _ _ _ _) => constructor.
Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
Forall3 P l1 k1 k1' Forall3 P l2 k2 k2'
......
......@@ -85,7 +85,7 @@ Instance: PartialOrder divide.
Proof.
repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
Qed.
Hint Extern 0 (_ | _) => reflexivity.
Hint Extern 0 (_ | _) => reflexivity : core.
Lemma Nat_divide_ne_0 x y : (x | y) y 0 x 0.
Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
......@@ -237,7 +237,7 @@ Instance N_le_po: PartialOrder (≤)%N.
Proof.
repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
Hint Extern 0 (_ _)%N => reflexivity.
Hint Extern 0 (_ _)%N => reflexivity : core.
(** * Notations and properties of [Z] *)
Open Scope Z_scope.
......@@ -391,7 +391,7 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.
Hint Extern 1 (_ _) => reflexivity || discriminate.
Hint Extern 1 (_ _) => reflexivity || discriminate : core.
Arguments Qred : simpl never.
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
......@@ -537,7 +537,7 @@ Close Scope Qc_scope.
(** The theory of positive rationals is very incomplete. We merely provide
some operations and theorems that are relevant for fractional permissions. *)
Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
Hint Resolve Qp_prf.
Hint Resolve Qp_prf : core.
Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
Arguments Qp_car _%Qp : assert.
......
......@@ -48,10 +48,10 @@ Proof. unfold is_Some. destruct mx; naive_solver. Qed.
Lemma mk_is_Some {A} (mx : option A) x : mx = Some x is_Some mx.
Proof. intros; red; subst; eauto. Qed.
Hint Resolve mk_is_Some.
Hint Resolve mk_is_Some : core.
Lemma is_Some_None {A} : ¬is_Some (@None A).
Proof. by destruct 1. Qed.
Hint Resolve is_Some_None.
Hint Resolve is_Some_None : core.
Lemma eq_None_not_Some {A} (mx : option A) : mx = None ¬is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
......
......@@ -13,8 +13,8 @@ From stdpp Require Export fin_maps.
Set Default Proof Using "Type".
Local Open Scope positive_scope.
Local Hint Extern 0 (_ =@{positive} _) => congruence.
Local Hint Extern 0 (_ @{positive} _) => congruence.
Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
Local Hint Extern 0 (_ @{positive} _) => congruence : core.
(** * The tree data structure *)
(** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
......@@ -41,14 +41,14 @@ Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf l.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) Pmap_wf r.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate Pmap_wf_l Pmap_wf_r.
Local Hint Immediate Pmap_wf_l Pmap_wf_r : core.
Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
Arguments PNode' : simpl never.
Lemma PNode_wf {A} o (l r : Pmap_raw A) :
Pmap_wf l Pmap_wf r Pmap_wf (PNode' o l r).
Proof. destruct o, l, r; simpl; auto. Qed.
Local Hint Resolve PNode_wf.
Local Hint Resolve PNode_wf : core.
(** Operations *)
Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
......
......@@ -57,13 +57,13 @@ End definitions.
(* Strongly normalizing elements *)
Notation sn R := (Acc (flip R)).
Hint Unfold nf red.
Hint Unfold nf red : core.
(** * General theorems *)
Section rtc.
Context `{R : relation A}.
Hint Constructors rtc nsteps bsteps tc.
Hint Constructors rtc nsteps bsteps tc : core.
(* We give this instance a lower-than-usual priority because [setoid_rewrite]
queries for [@Reflexive Prop ?r] in the hope of [iff_reflexive] getting
......
......@@ -32,7 +32,7 @@ Lemma not_elem_of_mkSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
Proof. done. Qed.
Lemma top_subseteq {A} (X : set A) : X .
Proof. done. Qed.
Hint Resolve top_subseteq.
Hint Resolve top_subseteq : core.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
Instance set_bind : MBind set := λ A B (f : A set B) (X : set A),
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment