Refactor the code to have a unique place for signature definition.
authorKim Nguyễn <kn@lri.fr>
Mon, 24 Sep 2012 16:25:40 +0000 (18:25 +0200)
committerKim Nguyễn <kn@lri.fr>
Mon, 24 Sep 2012 16:25:40 +0000 (18:25 +0200)
commitf5d90fb688bc1a9b29815fc33c369856e6c51a67
tree1512fd6c827c1e4548a299ab8168f39078a738cc
parent269daee8bbc5b86adeb9b23049c378e49cc82d2e
Refactor the code to have a unique place for signature definition.
Re-architecture the code to have all signatures in the sigs.ml module.
Any signature which occurs at least twice in the code (e.g. in a.ml
and corresponding a.mli) is put in a module A in Sigs. The signature
can the be included in a.ml and its 'module type of' can be included
in a.mli.

private signatures can stay in the .ml files where they appear.
13 files changed:
HACKING
src/finiteCofinite.ml
src/finiteCofinite.mli
src/formula.ml
src/formula.mli
src/hcons.ml
src/hcons.mli
src/ptset.ml
src/ptset.mli
src/qName.mli
src/sigs.ml
src/state.mli
src/utils.ml