Commit 93b578a5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'msammler/hintdb_discriminated' into 'master'

Create HintDBs with the discriminated option

See merge request iris/stdpp!148
parents dd919077 89eda68e
......@@ -2184,7 +2184,7 @@ Ltac decompose_map_disjoint := repeat
(** To prove a disjointness property, we first decompose all hypotheses, and
then use an auto database to prove the required property. *)
Create HintDb map_disjoint.
Create HintDb map_disjoint discriminated.
Ltac solve_map_disjoint :=
solve [decompose_map_disjoint; auto with map_disjoint].
......@@ -2258,7 +2258,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
rewrite E; clear E
end.
Create HintDb simpl_map.
Create HintDb simpl_map discriminated.
Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map map_disjoint.
Hint Extern 80 ((_ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
......
......@@ -73,7 +73,7 @@ of the forms:
- [N1 ## N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj.
Create HintDb ndisj discriminated.
(** Rules for goals of the form [_ ⊆ _] *)
(** If-and-only-if rules. Well, not quite, but for the fragment we are
......
Supports Markdown
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