Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-20 20:22:12 -0700 (Tue, 20 Apr 2004)
Revision: 5682
Log message:
(* WARNING : this breaks .prla/.cmoz binary compatibility, export ypur proofs *)
Include the resource types in the resource definition, not only in declaration.
The syntax of a resource implementation (in .ml) is being changed to
let resource (ctyp1, ctyp2) name = expr
where the types have the same meaning as in a resource declaration (in .mli)
It is now possible to implement a "private" resource w/o declaring it.
This fixes bug 168 (and its dup bug 178).