Commit 89eda68e authored by Michael Sammler's avatar Michael Sammler

Create HintDBs with the discriminated option

According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.
parent 2f540354
......@@ -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
......
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