diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-26 18:50:09 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-26 18:50:09 -0400 |
| commit | 91b0b095de58548e927c28550db376692b692c5b (patch) | |
| tree | cfe46d6a01c04d64b4540963e5455b90f2856fad /src | |
| parent | 055aff88a4d6c67f333735801ceac583c3761ba9 (diff) | |
Improve wf tactics
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/LanguageWf.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v index 2aac184ec..c2eb3805a 100644 --- a/src/Experiments/NewPipeline/LanguageWf.v +++ b/src/Experiments/NewPipeline/LanguageWf.v @@ -547,6 +547,8 @@ Module Compilers. | progress subst | progress inversion_sigma | progress inversion_prod + | progress destruct_head'_sig + | progress destruct_head'_and | progress cbn [List.In eq_rect] in * | match goal with | [ |- expr.wf _ _ _ ] => constructor |