Fix proofs broken by previous commit

2 files changed, 6 insertions, 2 deletions

diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v
index 4269cf09c..0fdb2e46c 100644
--- a/src/Compilers/Z/RewriteAddToAdcInterp.v
+++ b/src/Compilers/Z/RewriteAddToAdcInterp.v
@@ -42,7 +42,7 @@ Section language.
                 | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Interp ?interp_op' ?e ?x ]
                   => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H
                 end
-              | intros; eapply (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb)
+              | intros; exact (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb)
               | progress split_andb
               | congruence
               | tauto
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