From c699fda384efb181b54420a8f16192c07b1f2b9b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 11 May 2013 14:19:59 +0200 Subject: [PATCH] Improve "decompose_Forall_hyps" tactic. --- theories/list.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/list.v b/theories/list.v index d874ece4..b3158b87 100644 --- a/theories/list.v +++ b/theories/list.v @@ -2703,10 +2703,11 @@ Ltac simplify_zip_equality := repeat Ltac decompose_Forall_hyps := repeat match goal with - | H : Forall _ [] |- _ => inversion H + | H : Forall _ [] |- _ => clear H | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H + | H : Forall _ ?l, H' : length ?l ≠0 |- _ => is_var l; destruct H; [done|] | H : Forall2 _ [] [] |- _ => clear H | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H) | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H) -- GitLab