diff options
Diffstat (limited to 'test-suite/modules/mod_decl.v')
| -rw-r--r-- | test-suite/modules/mod_decl.v | 50 |
1 files changed, 22 insertions, 28 deletions
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v index 867b8a11..aad493ce 100644 --- a/test-suite/modules/mod_decl.v +++ b/test-suite/modules/mod_decl.v @@ -1,55 +1,49 @@ Module Type SIG. - Definition A:Set. (*error*) - Axiom A:Set. + Axiom A : Set. End SIG. Module M0. - Definition A:Set. - Exact nat. - Save. + Definition A : Set. + exact nat. + Qed. End M0. -Module M1:SIG. - Definition A:=nat. +Module M1 : SIG. + Definition A := nat. End M1. -Module M2<:SIG. - Definition A:=nat. +Module M2 <: SIG. + Definition A := nat. End M2. -Module M3:=M0. +Module M3 := M0. -Module M4:SIG:=M0. +Module M4 : SIG := M0. -Module M5<:SIG:=M0. +Module M5 <: SIG := M0. -Module F[X:SIG]:=X. - - -Declare Module M6. +Module F (X: SIG) := X. Module Type T. - Declare Module M0. - Lemma A:Set (*error*). - Axiom A:Set. + Module M0. + Axiom A : Set. End M0. - Declare Module M1:SIG. + Declare Module M1: SIG. - Declare Module M2<:SIG. - Definition A:=nat. + Declare Module M2 <: SIG. + Definition A := nat. End M2. - Declare Module M3:=M0. + Module M3 := M0. - Declare Module M4:SIG:=M0. (* error *) + Module M4 : SIG := M0. - Declare Module M5<:SIG:=M0. + Module M5 <: SIG := M0. - Declare Module M6:=F M0. (* error *) + Module M6 := F M0. - Module M7. -End T.
\ No newline at end of file +End T. |