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

1 files changed, 11 insertions, 7 deletions

diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
index 94c344bb..a4f9d3a2 100644
--- a/test-suite/modules/ind.v
+++ b/test-suite/modules/ind.v
@@ -1,13 +1,17 @@
 Module Type SIG.
-  Inductive w:Set:=A:w.
-  Parameter f : w->w.
+  Inductive w : Set :=
+      A : w.
+  Parameter f : w -> w.
 End SIG.
 
-Module M:SIG.
-  Inductive w:Set:=A:w.
-  Definition f:=[x]Cases x of A => A end.
+Module M : SIG.
+  Inductive w : Set :=
+      A : w.
+  Definition f x := match x with
+                    | A => A
+                    end.
 End M.
 
-Module N:=M.
+Module N := M.
 
-Check (N.f M.A).
+Check (N.f M.A).
\ No newline at end of file