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

1 files changed, 16 insertions, 16 deletions

diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
index b5f0e730..32d85779 100644
--- a/test-suite/success/CaseAlias.v
+++ b/test-suite/success/CaseAlias.v
@@ -1,21 +1,21 @@
 (* This has been a bug reported by Y. Bertot *)
 Inductive expr : Set :=
-   b: expr -> expr ->  expr
- | u: expr ->  expr
- | a: expr
- | var: nat ->  expr .
+  | b : expr -> expr -> expr
+  | u : expr -> expr
+  | a : expr
+  | var : nat -> expr.
 
-Fixpoint f [t : expr] : expr :=
- Cases t of
- | (b t1 t2) => (b (f t1) (f t2))
- | a => a
- | x => (b t a)
- end.
+Fixpoint f (t : expr) : expr :=
+  match t with
+  | b t1 t2 => b (f t1) (f t2)
+  | a => a
+  | x => b t a
+  end.
 
-Fixpoint f2 [t : expr] : expr :=
- Cases t of
- | (b t1 t2) => (b (f2 t1) (f2 t2))
- | a => a
- | x => (b x a)
- end.
+Fixpoint f2 (t : expr) : expr :=
+  match t with
+  | b t1 t2 => b (f2 t1) (f2 t2)
+  | a => a
+  | x => b x a
+  end.