diff options
author | Jason Gross <jgross@mit.edu> | 2017-02-13 15:40:07 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-02-13 15:40:07 -0500 |
commit | d650bb93a89ed1794fb4393a9b478c41674f8b6f (patch) | |
tree | 4a87ed36758f975c3a2936810ca018653a131ac5 /src/Reflection/WfInversion.v | |
parent | 7df92d63082b27123267425b4840c4f681cef16f (diff) |
Split off inversion_wff for constr-only hyps
Diffstat (limited to 'src/Reflection/WfInversion.v')
-rw-r--r-- | src/Reflection/WfInversion.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v index 1f7046176..cdaa7ffb5 100644 --- a/src/Reflection/WfInversion.v +++ b/src/Reflection/WfInversion.v @@ -146,7 +146,7 @@ Ltac is_expr_constructor arg := | Return _ => idtac end. -Ltac inversion_wff_step := +Ltac inversion_wff_step_gen guard_tac := let postprocess H := (cbv [wff_code] in H; simpl in H; @@ -156,11 +156,13 @@ Ltac inversion_wff_step := end) in match goal with | [ H : wff _ ?x ?y |- _ ] - => is_expr_constructor x; is_expr_constructor y; - apply wff_encode in H; postprocess H - | [ H : wff _ ?x ?y |- _ ] - => first [ is_var x; is_var y; fail 1 - | idtac ]; + => guard_tac x y; apply wff_encode in H; postprocess H end. +Ltac inversion_wff_step_constr := + inversion_wff_step_gen ltac:(fun x y => is_expr_constructor x; is_expr_constructor y). +Ltac inversion_wff_step_var := + inversion_wff_step_gen ltac:(fun x y => first [ is_var x; is_var y; fail 1 | idtac ]). +Ltac inversion_wff_step := first [ inversion_wff_step_constr | inversion_wff_step_var ]. +Ltac inversion_wff_constr := repeat inversion_wff_step_constr. Ltac inversion_wff := repeat inversion_wff_step. |