diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-25 16:37:12 -0700 |
| commit | 53f5fa354a50cf82880a4dd382d0a5a2024956ba (patch) | |
| tree | ec6323401db2b8c07beca7aafcf961da32d90743 /Test/dafny0/runtest.bat | |
| parent | 9b20e96cc4ca31eff8128965def3284c650c572f (diff) | |
Dafny: fixed resolution bug for inductive datatypes (previous check did not handle generic datatypes correctly)
Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)
Diffstat (limited to 'Test/dafny0/runtest.bat')
| -rw-r--r-- | Test/dafny0/runtest.bat | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 608b7358..f9cd5a89 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,8 +17,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
- TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy NoTypeArgs.dfy
- SplitExpr.dfy
+ TypeParameters.dfy Datatypes.dfy Coinductive.dfy
+ TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
@@ -34,3 +34,5 @@ for %%f in (SmallTests.dfy LetExpr.dfy) do ( %DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
%DAFNY_EXE% /compile:0 %* out.tmp.dfy
)
+
+%DAFNY_EXE% %* Compilation.dfy
|