From d4b3bb61d84cb2cd831a43b65dc55ef25fa8abaa Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 29 Jan 2003 18:56:05 +0000 Subject: Added a file for testing modules of coq (new version 7.4). Plus some modification to better backtrack modules. --- coq/ex-module.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 coq/ex-module.v (limited to 'coq/ex-module.v') diff --git a/coq/ex-module.v b/coq/ex-module.v new file mode 100644 index 00000000..e9d42072 --- /dev/null +++ b/coq/ex-module.v @@ -0,0 +1,49 @@ + +Module M. + Module Type SIG. + Parameter T:Set. + Parameter x:T. + End SIG. + Module N:SIG. + Definition T:=nat. + Definition x:=O. + End N. +End M. + +Section toto. +Print M. +End toto. + + +Lemma toto : O=O. +Module N:=M. +Definition t:=M.N.T. +Trivial. +Save. + + +Module Type SPRYT. + Module N. + Definition T:=M.N.T. + Parameter x:T. + End N. +End SPRYT. + +Module K:SPRYT:=N. +Module K':SPRYT:=M. + +Lemma titi : O=O. +Module Type S:=SPRYT. +Module N':=M. +Trivial. +Save. + + +Module Type SIG. + Definition T:Set:=M.N.T. + Parameter x:T. + + Module N:SPRYT. +End SIG. + +Module J:M.SIG:=M.N. -- cgit v1.2.3