diff options
| -rw-r--r-- | test-suite/success/RecTutorial.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 3f8a7f3eb..d8f804246 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -1075,8 +1075,8 @@ Proof. apply vector_double_rect. simpl. destruct i; discriminate 1. - destruct i; simpl;auto. - injection 1; injection 1; subst a; subst b; auto. + destruct i; simpl;auto. + injection 1 as ->; injection 1 as ->; auto. Qed. Set Implicit Arguments. |