From 73c9ad1ff19915fbaf053119c5498ff1314e92e3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Nov 2015 17:47:24 +0100
Subject: Fixing output test Cases.v.

Not sure if this is really what is expected though.
---
 test-suite/output/Cases.out | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d478..f846f4ee10 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 x =>
-    (let b0 := b in
-     if b0 as b return (P b -> True)
+| AC H0 =>
+    let b0 := b in
+    (if b0 as b return (P b -> True)
      then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+     else fun _ : P false => Logic.I) H0
 end
      : B -> True
-- 
cgit v1.2.3