diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
| commit | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (patch) | |
| tree | d9cc893bc1289d8ad09b21f6a2242d31fa51ef70 /Source/Dafny/RefinementTransformer.cs | |
| parent | 129ab22811996b4b46cfbcc6eb3f4b97a95f5416 (diff) | |
Make reveal axioms from opaque functions quantify over layers
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 1500e37f..70fdae85 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -492,6 +492,8 @@ namespace Microsoft.Dafny }
moduleUnderConstruction = null;
}
+ public void PostCyclicityResolve(ModuleDefinition m) {
+ }
Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions, Attributes moreAttributes) {
Contract.Requires(tok != null);
Contract.Requires(moreBody == null || f is Predicate);
|