From f62060afc35df63ea0241bdc419623c814ab3941 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 Jan 2021 11:56:59 +0000 Subject: Add destruction to context match expressions --- src/common/Vericertlib.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/common') diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 4f6c6fa..f2754be 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -73,9 +73,12 @@ Ltac solve_by_invert := solve_by_inverts 1. Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := - match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? end. + match goal with + | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? + | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? + end. -Ltac auto_destruct x := destruct_with_eqn x; simpl in *; try discriminate; try congruence. +Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := repeat match goal with -- cgit