summaryrefslogtreecommitdiff
path: root/Test/dafny0/ModuleExport.dfy.expect
Commit message (Collapse)AuthorAge
* Update module export error messages. Also for "import Y" if there is at leastGravatar qunyanm2016-03-21
| | | | | one exported view, but no exported view is marked as default, then it is an error.
* Implement module export so we can export a subset of items defined in theGravatar qunyanm2016-01-29
module.