diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /test-suite/modules/Demo.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/Demo.v')
-rw-r--r-- | test-suite/modules/Demo.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1e9273f0..1f27fe1b 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -1,51 +1,51 @@ Module M. - Definition t:=nat. - Definition x:=O. + Definition t := nat. + Definition x := 0. End M. Print M.t. Module Type SIG. - Parameter t:Set. - Parameter x:t. + Parameter t : Set. + Parameter x : t. End SIG. -Module F[X:SIG]. - Definition t:=X.t->X.t. - Definition x:t. - Intro. - Exact X.x. +Module F (X: SIG). + Definition t := X.t -> X.t. + Definition x : t. + intro. + exact X.x. Defined. - Definition y:=X.x. + Definition y := X.x. End F. Module N := F M. Print N.t. -Eval Compute in N.t. +Eval compute in N.t. Module N' : SIG := N. Print N'.t. -Eval Compute in N'.t. +Eval compute in N'.t. Module N'' <: SIG := F N. Print N''.t. -Eval Compute in N''.t. +Eval compute in N''.t. -Eval Compute in N''.x. +Eval compute in N''.x. -Module N''' : SIG with Definition t:=nat->nat := N. +Module N''' : SIG with Definition t := nat -> nat := N. Print N'''.t. -Eval Compute in N'''.t. +Eval compute in N'''.t. Print N'''.x. |