Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 11 insertions, 6 deletions

diff --git a/test-suite/success/Case14.v b/test-suite/success/Case14.v
index edecee79..f106a64c 100644
--- a/test-suite/success/Case14.v
+++ b/test-suite/success/Case14.v
@@ -4,13 +4,18 @@
 Axiom bad : false = true.
 
 Definition try1 : False :=
-  <[b:bool][_:false=b](if b then False else True)>
-  Cases bad of refl_equal => I end.
+  match bad in (_ = b) return (if b then False else True) with
+  | refl_equal => I
+  end.
 
 Definition try2 : False :=
-  <[b:bool][_:false=b]((if b then False else True)::Prop)>
-  Cases bad of refl_equal => I end.
+  match bad in (_ = b) return ((if b then False else True):Prop) with
+  | refl_equal => I
+  end.
 
 Definition try3 : False :=
-  <[b:bool][_:false=b](([b':bool] if b' then False else True) b)>
-  Cases bad of refl_equal => I end.
+  match
+    bad in (_ = b) return ((fun b' : bool => if b' then False else True) b)
+  with
+  | refl_equal => I
+  end.