diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
| tree | e1542c8adb83ff297284eefc23a2703461713d9b /test-suite/modules/ind.v | |
| parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
| parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) | |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/modules/ind.v')
| -rw-r--r-- | test-suite/modules/ind.v | 18 |
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 |