From 015a5d5254cb46191e47d5092002a5cac0864a8d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 9 Jan 2017 09:17:02 +0100
Subject: [PATCH] Simplify the proof of init_prod.
---
theories/typing/tests/init_prod.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index fd2a7189..f8cd890a 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.
--
GitLab