summaryrefslogtreecommitdiff
path: root/compiler/InterpreterStatements.mli
diff options
context:
space:
mode:
authorSon HO2023-11-28 08:04:43 +0100
committerGitHub2023-11-28 08:04:43 +0100
commitb78850a81dfea78bc280f1b5b6d2fdcb421e386a (patch)
tree3a4807b26856c0c2e21f1a8a4cdf80da136c26ec /compiler/InterpreterStatements.mli
parentbacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (diff)
parenta3a3ab9723348e24f83073a52145128f34022265 (diff)
Merge pull request #46 from AeneasVerif/son_improves
Minor improvements for the extraction
Diffstat (limited to 'compiler/InterpreterStatements.mli')
-rw-r--r--compiler/InterpreterStatements.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index d84e8be6..3832d02f 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -10,7 +10,7 @@ open Cps
dummy variables, after ending the proper borrows of course) but the return
variable, move the return value out of the return variable, remove all the
local variables (but preserve the abstractions!), remove the
- {!constructor:env_elem.Frame} indicator delimiting the current frame and
+ {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and
handle the return value to the continuation.
If the boolean is false, we don't move the return value, and call the