Commit 0c1dfc5f authored by Joachim Bard's avatar Joachim Bard

adding some debug ltacs

parent 981aa890
Require Import Flover.Infra.Ltacs.
Require Import Flover.Infra.NatSet.
Require Import Flover.IntervalArithQ.
Ltac debug_auto :=
match goal with
| [ |- context[match ?t with Some _ => _ | None => _ end] ] => debug_term t
| [ |- context[if ?t then _ else _ ]] => debug_term t
end.
Ltac solve_set :=
match goal with
| [ |- context[ ?x mem ?S ]] => debug_term (x mem S)
end.
Ltac subset_tac :=
match goal with
| [ |- context[ isSupersetIntv ?new_iv ?iv ]] =>
let name := fresh "subset" in
let res := eval compute in (isSupersetIntv new_iv iv) in
assert (name : isSupersetIntv new_iv iv = res)
by (vm_compute; auto); rewrite name
end.
Ltac clear_if_true_once :=
match goal with
| [ H: _ = true |- _ ] => clear H
end.
Ltac clear_true := repeat clear_if_true_once.
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