From 561dbba4ce47aa1920b27a6fa3ea1fdb03835557 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Jun 2016 13:17:16 +0200
Subject: Test-suite fix to 1744e37 (injection in context).

Preserve a compatibility whether the Structural Injection flag is on
or not.
---
 test-suite/success/RecTutorial.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 3f8a7f3eb6..d8f8042465 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.
-- 
cgit v1.2.3