diff options
Diffstat (limited to 'src/Compilers/Z/RewriteAddToAdcWf.v')
| -rw-r--r-- | src/Compilers/Z/RewriteAddToAdcWf.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v index 3b9fb1ff5..cabe61b03 100644 --- a/src/Compilers/Z/RewriteAddToAdcWf.v +++ b/src/Compilers/Z/RewriteAddToAdcWf.v @@ -21,7 +21,11 @@ Section language. repeat first [ eapply @Wf_InterpToPHOAS with (t:=Arrow _ _) | progress split_andb | congruence - | intros; eapply @PositiveContextOk + | intros; + match goal with + | [ |- ContextDefinitions.ContextOk _ ] + => eapply @PositiveContextOk + end | solve [ auto | eapply @BinPos.Pos.eqb_eq ] | eapply @Wf_from_unit | eapply @dec_rel_of_bool_dec_rel |