From f4002e6c85f575fc8451adb80dba705795f0a0c9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Nov 2015 22:35:03 +0100
Subject: Using x in output test-suite Cases.v (cosmetic).

---
 test-suite/output/Cases.out | 4 ++--
 test-suite/output/Cases.v   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f846f4ee10..f44465456f 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -47,10 +47,10 @@ foo' = if A 0 then true else false
 f = 
 fun H : B =>
 match H with
-| AC H0 =>
+| AC x =>
     let b0 := b in
     (if b0 as b return (P b -> True)
      then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) H0
+     else fun _ : P false => Logic.I) x
 end
      : B -> True
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index a95b085ac0..a4d19d6930 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -72,7 +72,7 @@ Inductive B : Prop := AC : P b -> B.
 Definition f : B -> True.
 
 Proof.
-intros [].
+intros [x].
 destruct b as [|] ; exact Logic.I.
 Defined.
 
-- 
cgit v1.2.3