summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsCore.ml
diff options
context:
space:
mode:
authorSon HO2024-03-09 01:12:20 +0100
committerGitHub2024-03-09 01:12:20 +0100
commit14171474f9a4a45874d181cdb6567c7af7dc32cd (patch)
treef4c7dcd5b172e8922487dec83070e2c38e7b441a /compiler/InterpreterLoopsCore.ml
parent169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff)
parent46f2f1c0c4c37f089e42c82d76d79817101c5407 (diff)
Merge pull request #85 from AeneasVerif/son/fix_loops3
Fix some issues with the loops
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsCore.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index e663eb42..0bd57756 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -12,6 +12,7 @@ type updt_env_kind =
| AbsInRight of AbstractionId.id
| LoanInRight of BorrowId.id
| LoansInRight of BorrowId.Set.t
+[@@deriving show]
(** Utility exception *)
exception ValueMatchFailure of updt_env_kind