Commit ffe69a28 authored by Robbert Krebbers's avatar Robbert Krebbers

Hint database for set_solver.

parent 32cc2890
......@@ -265,6 +265,7 @@ Ltac set_unfold :=
[set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *)
Tactic Notation "set_solver" "by" tactic3(tac) :=
try done;
intros; setoid_subst;
set_unfold;
intros; setoid_subst;
......@@ -278,6 +279,10 @@ Tactic Notation "set_solver" := set_solver by idtac.
Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
Hint Extern 1000 (_ _) => set_solver : set_solver.
Hint Extern 1000 (_ _) => set_solver : set_solver.
Hint Extern 1000 (_ _) => set_solver : set_solver.
(** * Conversion of option and list *)
Definition of_option `{Singleton A C, Empty C} (mx : option A) : C :=
match mx with None => | Some x => {[ x ]} end.
......
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