diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v index fd2a718996f309cf202f86869fbefa8de3b3e958..f8cd890a92b0e7f2cc6db738a1debba94d9ecbb9 100644 --- a/theories/typing/tests/init_prod.v +++ b/theories/typing/tests/init_prod.v @@ -26,7 +26,7 @@ Section rebor. { apply (uninit_product_subtype [] [] [1;1]%nat). } intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl. eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own. - eapply (type_assign (own 2 (uninit 1))); try solve_typing. by apply write_own. + eapply type_assign; try solve_typing. by apply write_own. eapply type_delete; try solve_typing. eapply type_delete; try solve_typing. eapply (type_jump [_]); solve_typing.