From 4acb5ce2075799174b46a1c950ce2ee1ea55d484 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Jun 2016 11:50:17 -0700 Subject: Add [break_match] for hypotheses --- src/Util/Tactics.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 2324e1b34..fea7dfe16 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -56,13 +56,34 @@ Ltac break_match_step only_when := | [ |- appcontext[match ?e with _ => _ end] ] => only_when e; destruct e eqn:? end. +Ltac break_match_hyps_step only_when := + match goal with + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; is_var e; destruct e + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; + match type of e with + | sumbool _ _ => destruct e + end + | [ H : appcontext[if ?e then _ else _] |- _ ] + => only_when e; destruct e eqn:? + | [ H : appcontext[match ?e with _ => _ end] |- _ ] + => only_when e; destruct e eqn:? + end. Ltac break_match := repeat break_match_step ltac:(fun _ => idtac). +Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac). Ltac break_match_when_head_step T := break_match_step ltac:(fun e => let T' := type of e in let T' := head T' in constr_eq T T'). +Ltac break_match_hyps_when_head_step T := + break_match_hyps_step + ltac:(fun e => let T' := type of e in + let T' := head T' in + constr_eq T T'). Ltac break_match_when_head T := repeat break_match_when_head_step T. +Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T. Ltac free_in x y := idtac; -- cgit v1.2.3