From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/success/RecTutorial.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/success/RecTutorial.v')

diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 11fbf24d..d8f80424 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -831,7 +831,7 @@ Proof.
  intro n.
  apply nat_ind with (P:= fun n => n <> S n).
  discriminate.
- red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto.
 Qed.
 
 Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
@@ -1075,8 +1075,8 @@ Proof.
  apply vector_double_rect.
  simpl.
  destruct i; discriminate 1.
- destruct i; simpl;auto.
- injection 1; injection 2;intros; subst a; subst b; auto.
+ destruct i; simpl;auto. 
+ injection 1 as ->; injection 1 as ->; auto.
 Qed.
 
  Set Implicit Arguments.
-- 
cgit v1.2.3