diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2003-01-29 18:56:05 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2003-01-29 18:56:05 +0000 |
commit | d4b3bb61d84cb2cd831a43b65dc55ef25fa8abaa (patch) | |
tree | 2747f268bfc5d439931f41bd845e3ce9e236ed88 /coq/ex-module.v | |
parent | a87f482d11b56fd8d3bbe148e174c4010e327794 (diff) |
Added a file for testing modules of coq (new version 7.4). Plus some
modification to better backtrack modules.
Diffstat (limited to 'coq/ex-module.v')
-rw-r--r-- | coq/ex-module.v | 49 |
1 files changed, 49 insertions, 0 deletions
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. |