Using x in output test-suite Cases.v (cosmetic).

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.