From 06e57f092923313915e128032c11738068ff8db2 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 20 Feb 2003 17:37:33 +0000 Subject: corrected a bug of pg/coq, the following line was not recognized as a module start: Module M:T with Definition A:=u. I had to count the number of 'with' and ':=' to know if the last ':=' was a Module given explicitely (--> no module start) or only part of a 'with ...:=' (--> module start). --- coq/ex-module.v | 40 ++++++++++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 6 deletions(-) (limited to 'coq/ex-module.v') diff --git a/coq/ex-module.v b/coq/ex-module.v index f8df0c31..227b3ff7 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -1,4 +1,27 @@ +Module Type O1. +Parameter A:Set. +Parameter B:Set. +End O1. + + +Module R:O1. +Definition A:=nat. +Definition B:=bool. +End R. + +Module R2: O1 with Definition A:=nat. +Definition A:=nat. +Definition B:=bool. +End R2. + +Module R4. +Module R3: O1 with Definition A:=nat :=R2. +End R4. + + + + Module M. Module Type SIG. Parameter T:Set. @@ -15,6 +38,10 @@ Module M. Module O:=N. End M. +Import M. +Print t. + + Definition t:O=O. Trivial. Save. @@ -24,13 +51,14 @@ Section toto. Print M. End toto. - Module N:=M. +Module N:=M. + + +Module Type typ. +Parameter T:Set. +Parameter a:T. +End typ. -Module R:N.SIG. - Definition T:Set:=nat. - Definition x:T:= O. - Definition foo:nat:=(S O). -End R. Module Type N'. -- cgit v1.2.3