diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-24 02:19:35 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-24 02:19:35 -0400 |
| commit | 181732cac3ebaa957ecba638ade464611b1a6b17 (patch) | |
| tree | a8b65a84564650131b5c05037201230a8142ed3d /src/Compilers/WfInversion.v | |
| parent | c1944b67c24530e92b04f49a6c64b95e667272c4 (diff) | |
Add inversion_wf_one_constr
Diffstat (limited to 'src/Compilers/WfInversion.v')
| -rw-r--r-- | src/Compilers/WfInversion.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/WfInversion.v b/src/Compilers/WfInversion.v index 79869e554..bf8c93ade 100644 --- a/src/Compilers/WfInversion.v +++ b/src/Compilers/WfInversion.v @@ -198,8 +198,11 @@ Ltac inversion_wf_step_gen guard_tac := end. Ltac inversion_wf_step_constr := inversion_wf_step_gen ltac:(fun x y => is_expr_constructor x; is_expr_constructor y). +Ltac inversion_wf_step_one_constr := + inversion_wf_step_gen ltac:(fun x y => first [ is_expr_constructor x | is_expr_constructor y]). Ltac inversion_wf_step_var := inversion_wf_step_gen ltac:(fun x y => first [ is_var x; is_var y; fail 1 | idtac ]). Ltac inversion_wf_step := first [ inversion_wf_step_constr | inversion_wf_step_var ]. Ltac inversion_wf_constr := repeat inversion_wf_step_constr. +Ltac inversion_wf_one_constr := repeat inversion_wf_step_one_constr. Ltac inversion_wf := repeat inversion_wf_step. |