diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-12 17:59:29 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-12 17:59:43 -0500 |
| commit | d05f8ec1acb3935af95c80f502af6f2f1fdd5bf6 (patch) | |
| tree | 73c17dd7f0163d89d21f9f864441b5749144dfb9 /src | |
| parent | 58fbde3bf3095d937ad55b11ba3eae6960c1f3e7 (diff) | |
Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565d
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf2.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index ec6142103..142f953fa 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -206,7 +206,8 @@ Module Compilers. | [ H : option_eq ?R ?x ?y |- _ ] => destruct x eqn:?, y eqn:?; cbv [option_eq] in H | [ |- wf_unification_resultT' _ (_, _) (_, _) ] => split; assumption - end ]. + end + | progress cbv [Option.bind] in * ]. Qed. Lemma wf_unify_pattern |